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  1361  19.36  1819  sblim  2021  sban  2022  sbhb  2059  2sb6  2065  2sb6rf  2070  eu1  2177  moabs  2200  moanim  2212  2eu6  2241  r2alf  2591  r19.21t  2641  r19.35  2700  reu2  2966  reu8  2974  2reu5lem3  2985  ssconb  3322  ssin  3404  difin  3419  reldisj  3511  ssundif  3550  pwpw0  3779  pwsnALT  3838  unissb  3873  moabex  4248  dffr2  4374  dfepfr  4394  ssrel  4792  dffr3  5061  fncnv  5330  fun11  5331  dff13  5799  marypha2lem3  7206  dfsup2  7211  wemapso2lem  7281  inf2  7340  axinf2  7357  aceq1  7760  aceq0  7761  kmlem14  7805  dfackm  7808  zfac  8102  ac6n  8128  zfcndrep  8252  zfcndac  8257  axgroth6  8466  axgroth4  8470  grothprim  8472  prime  10108  raluz2  10284  rpnnen2  12520  isprm2  12782  isprm4  12784  pgpfac1  15331  pgpfac  15335  isirred2  15499  isclo2  16841  lmres  17044  ist1-2  17091  is1stc2  17184  alexsubALTlem3  17759  itg2cn  19134  ellimc3  19245  plydivex  19693  vieta1  19708  dchrelbas2  20492  nmobndseqi  21373  nmobndseqiOLD  21374  cvnbtwn3  22884  elat2  22936  ballotlemfc0  23067  ballotlemfcc  23068  bisimpd  23136  funcnvmptOLD  23249  funcnvmpt  23250  xrofsup  23270  disjrdx  23385  esumpcvgval  23461  esumcvg  23469  axinfprim  24067  dfon2lem9  24218  dffr4  24253  dffun10  24524  df3nandALT1  24907  df3nandALT2  24908  ltl4ev  25095  elicc3  26331  dfcon2OLD  26356  filnetlem4  26433  raldifsni  26856  dford4  27225  pm10.541  27665  pm13.196a  27717  2sbc6g  27718  wallispilem4  27920  wallispi2lem1  27923  rmoanim  28060  impexp3a  28574  bnj1098  29131  bnj1533  29200  bnj121  29218  bnj124  29219  bnj130  29222  bnj153  29228  bnj207  29229  bnj611  29266  bnj864  29270  bnj865  29271  bnj1000  29289  bnj978  29297  bnj1021  29312  bnj1047  29319  bnj1049  29320  bnj1090  29325  bnj1110  29328  bnj1128  29336  bnj1145  29339  bnj1171  29346  bnj1172  29347  bnj1174  29349  bnj1176  29351  bnj1280  29366  sblimNEW7  29543  sbanNEW7  29544  sbhbwAUX7  29579  2sb6NEW7  29582  sbhbOLD7  29714  2sb6rfOLD7  29718  a12peros  29743  lcvnbtwn3  29840  isat3  30119  cdleme25cv  31169  cdlemefrs29bpre0  31207  cdlemk35  31723
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