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

Theorem imbi2i 225
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  |-  ( ph  <->  ps )
Assertion
Ref Expression
imbi2i  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )

Proof of Theorem imbi2i
StepHypRef Expression
1 bi.a . . 3  |-  ( ph  <->  ps )
21a1i 9 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.74i 179 1  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imbi12i  238  anidmdbi  395  nan  666  sbcof2  1766  sblimv  1850  sbhb  1893  sblim  1908  2sb6  1937  sbcom2v  1938  2sb6rf  1943  eu1  2002  moabs  2026  mo3h  2030  moanim  2051  2moswapdc  2067  r2alf  2429  r19.21t  2484  rspc2gv  2775  reu2  2845  reu8  2853  2reuswapdc  2861  2rmorex  2863  dfdif3  3156  ssconb  3179  ssin  3268  reldisj  3384  ssundifim  3416  ralm  3437  unissb  3736  repizf2lem  4055  elirr  4426  en2lp  4439  tfi  4466  ssrel  4597  ssrel2  4599  fncnv  5159  fun11  5160  axcaucvglemres  7675  axpre-suploc  7678  suprzclex  9117  raluz2  9342  supinfneg  9358  infsupneg  9359  infssuzex  11569  bezoutlemmain  11613  isprm2  11725  lmres  12344  limcdifap  12727
  Copyright terms: Public domain W3C validator