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  659  sbcof2  1732  sblimv  1816  sbhb  1858  sblim  1873  2sb6  1902  sbcom2v  1903  2sb6rf  1908  eu1  1967  moabs  1991  mo3h  1995  moanim  2016  2moswapdc  2032  r2alf  2384  r19.21t  2437  rspc2gv  2713  reu2  2781  reu8  2789  2reuswapdc  2795  2rmorex  2797  ssconb  3106  ssin  3195  reldisj  3302  ssundifim  3333  ralm  3353  unissb  3639  repizf2lem  3943  elirr  4292  en2lp  4305  tfi  4331  ssrel  4454  ssrel2  4456  fncnv  4996  fun11  4997  axcaucvglemres  7127  suprzclex  8526  raluz2  8748  supinfneg  8764  infsupneg  8765  infssuzex  10489  bezoutlemmain  10531  isprm2  10643
  Copyright terms: Public domain W3C validator