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

Theorem imbi2i 303
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 10 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.74i 236 1  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12i  316  iman  413  pm4.14  561  nan  563  pm5.32  617  anidmdbi  627  imimorb  847  pm5.6  878  exp3acom23g  1371  19.36  1874  sblim  2073  sban  2074  sbhb  2112  2sb6  2118  2sb6rf  2123  eu1  2230  moabs  2253  moanim  2265  2eu6  2294  axi12  2338  r2alf  2654  r19.21t  2704  r19.35  2763  reu2  3029  reu8  3037  2reu5lem3  3048  ssconb  3385  ssin  3467  difin  3482  reldisj  3574  ssundif  3613  pwpw0  3842  pwsnALT  3901  unissb  3936  moabex  4311  dffr2  4437  dfepfr  4457  ssrel  4855  dffr3  5124  fncnv  5393  fun11  5394  dff13  5867  marypha2lem3  7277  dfsup2  7282  wemapso2lem  7352  inf2  7411  axinf2  7428  aceq1  7831  aceq0  7832  kmlem14  7876  dfackm  7879  zfac  8173  ac6n  8199  zfcndrep  8323  zfcndac  8328  axgroth6  8537  axgroth4  8541  grothprim  8543  prime  10181  raluz2  10357  rpnnen2  12595  isprm2  12857  isprm4  12859  pgpfac1  15408  pgpfac  15412  isirred2  15576  isclo2  16925  lmres  17128  ist1-2  17175  is1stc2  17268  alexsubALTlem3  17839  itg2cn  19216  ellimc3  19327  plydivex  19775  vieta1  19790  dchrelbas2  20582  nmobndseqi  21465  nmobndseqiOLD  21466  cvnbtwn3  22976  elat2  23028  bisimpd  23135  disjrdx  23226  funcnvmptOLD  23282  funcnvmpt  23283  xrofsup  23324  esumpcvgval  23734  esumcvg  23742  ballotlemfc0  23999  ballotlemfcc  24000  axinfprim  24456  dfon2lem9  24705  dffr4  24740  dffun10  25011  df3nandALT1  25394  df3nandALT2  25395  elicc3  25552  dfcon2OLD  25577  filnetlem4  25654  raldifsni  26076  dford4  26445  pm10.541  26885  pm13.196a  26937  2sbc6g  26938  wallispilem4  27140  wallispi2lem1  27143  rmoanim  27280  impexp3a  28003  bnj1098  28560  bnj1533  28629  bnj121  28647  bnj124  28648  bnj130  28651  bnj153  28657  bnj207  28658  bnj611  28695  bnj864  28699  bnj865  28700  bnj1000  28718  bnj978  28726  bnj1021  28741  bnj1047  28748  bnj1049  28749  bnj1090  28754  bnj1110  28757  bnj1128  28765  bnj1145  28768  bnj1171  28775  bnj1172  28776  bnj1174  28778  bnj1176  28780  bnj1280  28795  sblimNEW7  28972  sbanNEW7  28973  sbhbwAUX7  29008  2sb6NEW7  29011  sbhbOLD7  29144  2sb6rfOLD7  29148  a12peros  29173  lcvnbtwn3  29270  isat3  29549  cdleme25cv  30599  cdlemefrs29bpre0  30637  cdlemk35  31153
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 177
  Copyright terms: Public domain W3C validator