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  2102  sban  2103  sbhb  2141  2sb6  2147  2sb6rf  2153  eu1  2260  moabs  2283  moanim  2295  2eu6  2324  r2alf  2685  r19.21t  2735  r19.35  2799  reu2  3066  reu8  3074  2reu5lem3  3085  ssconb  3424  ssin  3507  difin  3522  reldisj  3615  ssundif  3655  pwpw0  3890  pwsnALT  3953  unissb  3988  moabex  4364  dffr2  4489  dfepfr  4509  ssrel  4905  ssrel2  4907  dffr3  5177  fncnv  5456  fun11  5457  dff13  5944  marypha2lem3  7378  dfsup2  7383  wemapso2lem  7453  inf2  7512  axinf2  7529  aceq1  7932  aceq0  7933  kmlem14  7977  dfackm  7980  zfac  8274  ac6n  8299  zfcndrep  8423  zfcndac  8428  axgroth6  8637  axgroth4  8641  grothprim  8643  prime  10283  raluz2  10459  rpnnen2  12753  isprm2  13015  isprm4  13017  pgpfac1  15566  pgpfac  15570  isirred2  15734  isclo2  17076  lmres  17287  ist1-2  17334  is1stc2  17427  alexsubALTlem3  18002  itg2cn  19523  ellimc3  19634  plydivex  20082  vieta1  20097  dchrelbas2  20889  nmobndseqi  22129  nmobndseqiOLD  22130  cvnbtwn3  23640  elat2  23692  funcnvmptOLD  23924  axinfprim  24935  dfon2lem9  25172  dffr4  25207  dffun10  25478  df3nandALT1  25861  df3nandALT2  25862  elicc3  26012  filnetlem4  26102  raldifsni  26426  dford4  26792  pm10.541  27232  pm13.196a  27284  2sbc6g  27285  rmoanim  27626  sbidd-misc  27809  impexp3a  27940  bnj1098  28493  bnj1533  28562  bnj121  28580  bnj124  28581  bnj130  28584  bnj153  28590  bnj207  28591  bnj611  28628  bnj864  28632  bnj865  28633  bnj1000  28651  bnj978  28659  bnj1021  28674  bnj1047  28681  bnj1049  28682  bnj1090  28687  bnj1110  28690  bnj1128  28698  bnj1145  28701  bnj1171  28708  bnj1172  28709  bnj1174  28711  bnj1176  28713  bnj1280  28728  sblimNEW7  28905  sbanNEW7  28906  sbhbwAUX7  28941  2sb6NEW7  28944  sbhbOLD7  29077  2sb6rfOLD7  29080  lcvnbtwn3  29144  isat3  29423  cdleme25cv  30473  cdlemefrs29bpre0  30511  cdlemk35  31027
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