MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2i Structured version   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  1380  19.36  1892  sblim  2142  sban  2143  sbhb  2182  2sb6  2188  2sb6rf  2194  eu1  2301  moabs  2324  moanim  2336  2eu6  2365  r2alf  2732  r19.21t  2783  r19.35  2847  reu2  3114  reu8  3122  2reu5lem3  3133  ssconb  3472  ssin  3555  difin  3570  reldisj  3663  ssundif  3703  pwpw0  3938  pwsnALT  4002  unissb  4037  moabex  4414  dffr2  4539  dfepfr  4559  ssrel  4956  ssrel2  4958  dffr3  5228  fncnv  5507  fun11  5508  dff13  5996  marypha2lem3  7434  dfsup2  7439  wemapso2lem  7509  inf2  7568  axinf2  7585  aceq1  7988  aceq0  7989  kmlem14  8033  dfackm  8036  zfac  8330  ac6n  8355  zfcndrep  8479  zfcndac  8484  axgroth6  8693  axgroth4  8697  grothprim  8699  prime  10340  raluz2  10516  rpnnen2  12815  isprm2  13077  isprm4  13079  pgpfac1  15628  pgpfac  15632  isirred2  15796  isclo2  17142  lmres  17354  ist1-2  17401  is1stc2  17495  alexsubALTlem3  18070  itg2cn  19645  ellimc3  19756  plydivex  20204  vieta1  20219  dchrelbas2  21011  nmobndseqi  22270  nmobndseqiOLD  22271  cvnbtwn3  23781  elat2  23833  funcnvmptOLD  24072  isarchi2  24245  axinfprim  25145  dfon2lem9  25406  dffr4  25442  dffun10  25724  df3nandALT1  26111  df3nandALT2  26112  elicc3  26274  filnetlem4  26364  raldifsni  26688  dford4  27054  pm10.541  27494  pm13.196a  27546  2sbc6g  27547  rmoanim  27888  sbidd-misc  28363  impexp3a  28497  bnj1098  29055  bnj1533  29124  bnj121  29142  bnj124  29143  bnj130  29146  bnj153  29152  bnj207  29153  bnj611  29190  bnj864  29194  bnj865  29195  bnj1000  29213  bnj978  29221  bnj1021  29236  bnj1047  29243  bnj1049  29244  bnj1090  29249  bnj1110  29252  bnj1128  29260  bnj1145  29263  bnj1171  29270  bnj1172  29271  bnj1174  29273  bnj1176  29275  bnj1280  29290  sblimNEW7  29469  sbanNEW7  29470  sbhbwAUX7  29508  2sb6NEW7  29511  sbhbOLD7  29661  2sb6rfOLD7  29663  lcvnbtwn3  29727  isat3  30006  cdleme25cv  31056  cdlemefrs29bpre0  31094  cdlemk35  31610
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