MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2i Unicode version

Theorem imbi2i 304
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 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.74i 237 1  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imbi12i  317  iman  414  pm4.14  562  nan  564  pm5.32  618  anidmdbi  628  imimorb  848  pm5.6  879  exp3acom23g  1377  19.36  1888  sblim  2125  sban  2126  sbhb  2164  2sb6  2170  2sb6rf  2176  eu1  2283  moabs  2306  moanim  2318  2eu6  2347  r2alf  2709  r19.21t  2759  r19.35  2823  reu2  3090  reu8  3098  2reu5lem3  3109  ssconb  3448  ssin  3531  difin  3546  reldisj  3639  ssundif  3679  pwpw0  3914  pwsnALT  3978  unissb  4013  moabex  4390  dffr2  4515  dfepfr  4535  ssrel  4931  ssrel2  4933  dffr3  5203  fncnv  5482  fun11  5483  dff13  5971  marypha2lem3  7408  dfsup2  7413  wemapso2lem  7483  inf2  7542  axinf2  7559  aceq1  7962  aceq0  7963  kmlem14  8007  dfackm  8010  zfac  8304  ac6n  8329  zfcndrep  8453  zfcndac  8458  axgroth6  8667  axgroth4  8671  grothprim  8673  prime  10314  raluz2  10490  rpnnen2  12788  isprm2  13050  isprm4  13052  pgpfac1  15601  pgpfac  15605  isirred2  15769  isclo2  17115  lmres  17326  ist1-2  17373  is1stc2  17466  alexsubALTlem3  18041  itg2cn  19616  ellimc3  19727  plydivex  20175  vieta1  20190  dchrelbas2  20982  nmobndseqi  22241  nmobndseqiOLD  22242  cvnbtwn3  23752  elat2  23804  funcnvmptOLD  24043  isarchi2  24216  axinfprim  25116  dfon2lem9  25369  dffr4  25404  dffun10  25675  df3nandALT1  26058  df3nandALT2  26059  elicc3  26218  filnetlem4  26308  raldifsni  26632  dford4  26998  pm10.541  27438  pm13.196a  27490  2sbc6g  27491  rmoanim  27832  sbidd-misc  28184  impexp3a  28315  bnj1098  28872  bnj1533  28941  bnj121  28959  bnj124  28960  bnj130  28963  bnj153  28969  bnj207  28970  bnj611  29007  bnj864  29011  bnj865  29012  bnj1000  29030  bnj978  29038  bnj1021  29053  bnj1047  29060  bnj1049  29061  bnj1090  29066  bnj1110  29069  bnj1128  29077  bnj1145  29080  bnj1171  29087  bnj1172  29088  bnj1174  29090  bnj1176  29092  bnj1280  29107  sblimNEW7  29284  sbanNEW7  29285  sbhbwAUX7  29320  2sb6NEW7  29323  sbhbOLD7  29456  2sb6rfOLD7  29459  lcvnbtwn3  29523  isat3  29802  cdleme25cv  30852  cdlemefrs29bpre0  30890  cdlemk35  31406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator