Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi2i GIF version

Theorem imbi2i 215
 Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
Hypothesis
Ref Expression
bi.a (𝜑𝜓)
Assertion
Ref Expression
imbi2i ((𝜒𝜑) ↔ (𝜒𝜓))

Proof of Theorem imbi2i
StepHypRef Expression
1 bi.a . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
32pm5.74i 169 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  imbi12i  228  anidmdbi  378  nan  626  sbcof2  1691  sblimv  1774  sbhb  1816  sblim  1831  2sb6  1860  sbcom2v  1861  2sb6rf  1866  eu1  1925  moabs  1949  mo3h  1953  moanim  1974  2moswapdc  1990  r2alf  2341  r19.21t  2394  reu2  2729  reu8  2737  2reuswapdc  2743  2rmorex  2745  ssconb  3076  ssin  3159  reldisj  3271  ssundifim  3306  ralm  3325  unissb  3610  repizf2lem  3914  elirr  4266  en2lp  4278  tfi  4305  ssrel  4428  ssrel2  4430  fncnv  4965  fun11  4966  axcaucvglemres  6973  raluz2  8522
 Copyright terms: Public domain W3C validator