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

Theorem imbi2i 224
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 178 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imbi12i  237  anidmdbi  390  nan  661  sbcof2  1738  sblimv  1822  sbhb  1864  sblim  1879  2sb6  1908  sbcom2v  1909  2sb6rf  1914  eu1  1973  moabs  1997  mo3h  2001  moanim  2022  2moswapdc  2038  r2alf  2395  r19.21t  2448  rspc2gv  2733  reu2  2803  reu8  2811  2reuswapdc  2819  2rmorex  2821  dfdif3  3110  ssconb  3133  ssin  3222  reldisj  3334  ssundifim  3366  ralm  3386  unissb  3683  repizf2lem  3996  elirr  4357  en2lp  4370  tfi  4397  ssrel  4526  ssrel2  4528  fncnv  5080  fun11  5081  axcaucvglemres  7432  suprzclex  8842  raluz2  9065  supinfneg  9081  infsupneg  9082  infssuzex  11219  bezoutlemmain  11261  isprm2  11373
  Copyright terms: Public domain W3C validator