ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi2i Unicode 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  |-  ( 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 178 1  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )
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  2732  reu2  2801  reu8  2809  2reuswapdc  2817  2rmorex  2819  dfdif3  3108  ssconb  3131  ssin  3220  reldisj  3331  ssundifim  3362  ralm  3382  unissb  3678  repizf2lem  3988  elirr  4347  en2lp  4360  tfi  4387  ssrel  4514  ssrel2  4516  fncnv  5066  fun11  5067  axcaucvglemres  7413  suprzclex  8814  raluz2  9036  supinfneg  9052  infsupneg  9053  infssuzex  11027  bezoutlemmain  11069  isprm2  11181
  Copyright terms: Public domain W3C validator