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  1807  sblim  2008  sban  2009  sbhb  2046  2sb6  2052  2sb6rf  2057  eu1  2164  moabs  2187  moanim  2199  2eu6  2228  r2alf  2578  r19.21t  2628  r19.35  2687  reu2  2953  reu8  2961  2reu5lem3  2972  ssconb  3309  ssin  3391  difin  3406  reldisj  3498  ssundif  3537  pwpw0  3763  pwsnALT  3822  unissb  3857  moabex  4232  dffr2  4358  dfepfr  4378  ssrel  4776  dffr3  5045  fncnv  5314  fun11  5315  dff13  5783  marypha2lem3  7190  dfsup2  7195  wemapso2lem  7265  inf2  7324  axinf2  7341  aceq1  7744  aceq0  7745  kmlem14  7789  dfackm  7792  zfac  8086  ac6n  8112  zfcndrep  8236  zfcndac  8241  axgroth6  8450  axgroth4  8454  grothprim  8456  prime  10092  raluz2  10268  rpnnen2  12504  isprm2  12766  isprm4  12768  pgpfac1  15315  pgpfac  15319  isirred2  15483  isclo2  16825  lmres  17028  ist1-2  17075  is1stc2  17168  alexsubALTlem3  17743  itg2cn  19118  ellimc3  19229  plydivex  19677  vieta1  19692  dchrelbas2  20476  nmobndseqi  21357  nmobndseqiOLD  21358  cvnbtwn3  22868  elat2  22920  ballotlemfc0  23051  ballotlemfcc  23052  bisimpd  23120  funcnvmptOLD  23234  funcnvmpt  23235  xrofsup  23255  disjrdx  23370  esumpcvgval  23446  esumcvg  23454  axinfprim  24052  dfon2lem9  24147  dffr4  24182  dffun10  24453  df3nandALT1  24835  df3nandALT2  24836  ltl4ev  24992  elicc3  26228  dfcon2OLD  26253  filnetlem4  26330  raldifsni  26753  dford4  27122  pm10.541  27562  pm13.196a  27614  2sbc6g  27615  wallispilem4  27817  wallispi2lem1  27820  rmoanim  27957  impexp3a  28275  bnj1098  28815  bnj1533  28884  bnj121  28902  bnj124  28903  bnj130  28906  bnj153  28912  bnj207  28913  bnj611  28950  bnj864  28954  bnj865  28955  bnj1000  28973  bnj978  28981  bnj1021  28996  bnj1047  29003  bnj1049  29004  bnj1090  29009  bnj1110  29012  bnj1128  29020  bnj1145  29023  bnj1171  29030  bnj1172  29031  bnj1174  29033  bnj1176  29035  bnj1280  29050  a12peros  29121  lcvnbtwn3  29218  isat3  29497  cdleme25cv  30547  cdlemefrs29bpre0  30585  cdlemk35  31101
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