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  1881  sblim  2101  sban  2102  sbhb  2140  2sb6  2146  2sb6rf  2152  eu1  2259  moabs  2282  moanim  2294  2eu6  2323  r2alf  2684  r19.21t  2734  r19.35  2798  reu2  3065  reu8  3073  2reu5lem3  3084  ssconb  3423  ssin  3506  difin  3521  reldisj  3614  ssundif  3654  pwpw0  3889  pwsnALT  3952  unissb  3987  moabex  4363  dffr2  4488  dfepfr  4508  ssrel  4904  ssrel2  4906  dffr3  5176  fncnv  5455  fun11  5456  dff13  5943  marypha2lem3  7377  dfsup2  7382  wemapso2lem  7452  inf2  7511  axinf2  7528  aceq1  7931  aceq0  7932  kmlem14  7976  dfackm  7979  zfac  8273  ac6n  8298  zfcndrep  8422  zfcndac  8427  axgroth6  8636  axgroth4  8640  grothprim  8642  prime  10282  raluz2  10458  rpnnen2  12752  isprm2  13014  isprm4  13016  pgpfac1  15565  pgpfac  15569  isirred2  15733  isclo2  17075  lmres  17286  ist1-2  17333  is1stc2  17426  alexsubALTlem3  18001  itg2cn  19522  ellimc3  19633  plydivex  20081  vieta1  20096  dchrelbas2  20888  nmobndseqi  22128  nmobndseqiOLD  22129  cvnbtwn3  23639  elat2  23691  funcnvmptOLD  23923  axinfprim  24934  dfon2lem9  25171  dffr4  25206  dffun10  25477  df3nandALT1  25860  df3nandALT2  25861  elicc3  26011  filnetlem4  26101  raldifsni  26425  dford4  26791  pm10.541  27231  pm13.196a  27283  2sbc6g  27284  rmoanim  27625  sbidd-misc  27808  impexp3a  27939  bnj1098  28492  bnj1533  28561  bnj121  28579  bnj124  28580  bnj130  28583  bnj153  28589  bnj207  28590  bnj611  28627  bnj864  28631  bnj865  28632  bnj1000  28650  bnj978  28658  bnj1021  28673  bnj1047  28680  bnj1049  28681  bnj1090  28686  bnj1110  28689  bnj1128  28697  bnj1145  28700  bnj1171  28707  bnj1172  28708  bnj1174  28710  bnj1176  28712  bnj1280  28727  sblimNEW7  28904  sbanNEW7  28905  sbhbwAUX7  28940  2sb6NEW7  28943  sbhbOLD7  29076  2sb6rfOLD7  29079  lcvnbtwn3  29143  isat3  29422  cdleme25cv  30472  cdlemefrs29bpre0  30510  cdlemk35  31026
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