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

Theorem imbi2i 219
 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 173 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  imbi12i  232  anidmdbi  384  nan  636  sbcof2  1707  sblimv  1790  sbhb  1832  sblim  1847  2sb6  1876  sbcom2v  1877  2sb6rf  1882  eu1  1941  moabs  1965  mo3h  1969  moanim  1990  2moswapdc  2006  r2alf  2358  r19.21t  2411  rspc2gv  2684  reu2  2752  reu8  2760  2reuswapdc  2766  2rmorex  2768  ssconb  3104  ssin  3187  reldisj  3299  ssundifim  3334  ralm  3353  unissb  3638  repizf2lem  3942  elirr  4294  en2lp  4306  tfi  4333  ssrel  4456  ssrel2  4458  fncnv  4993  fun11  4994  axcaucvglemres  7031  raluz2  8618
 Copyright terms: Public domain W3C validator