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  2137  sban  2139  sbhb  2183  2sb6  2189  2sb6rf  2195  eu1  2302  moabs  2325  moanim  2337  2eu6  2366  r2alf  2740  r19.21t  2791  r19.35  2855  reu2  3122  reu8  3130  2reu5lem3  3141  ssconb  3480  ssin  3563  difin  3578  reldisj  3671  ssundif  3711  pwpw0  3946  pwsnALT  4010  unissb  4045  moabex  4422  dffr2  4547  dfepfr  4567  ssrel  4964  ssrel2  4966  dffr3  5236  fncnv  5515  fun11  5516  dff13  6004  marypha2lem3  7442  dfsup2  7447  wemapso2lem  7519  inf2  7578  axinf2  7595  aceq1  7998  aceq0  7999  kmlem14  8043  dfackm  8046  zfac  8340  ac6n  8365  zfcndrep  8489  zfcndac  8494  axgroth6  8703  axgroth4  8707  grothprim  8709  prime  10350  raluz2  10526  rpnnen2  12825  isprm2  13087  isprm4  13089  pgpfac1  15638  pgpfac  15642  isirred2  15806  isclo2  17152  lmres  17364  ist1-2  17411  is1stc2  17505  alexsubALTlem3  18080  itg2cn  19655  ellimc3  19766  plydivex  20214  vieta1  20229  dchrelbas2  21021  nmobndseqi  22280  nmobndseqiOLD  22281  cvnbtwn3  23791  elat2  23843  funcnvmptOLD  24082  isarchi2  24255  axinfprim  25155  dfon2lem9  25418  dffr4  25457  dffun10  25759  df3nandALT1  26146  df3nandALT2  26147  elicc3  26320  filnetlem4  26410  raldifsni  26734  dford4  27100  pm10.541  27539  pm13.196a  27591  2sbc6g  27592  rmoanim  27933  sbidd-misc  28462  impexp3a  28596  bnj1098  29154  bnj1533  29223  bnj121  29241  bnj124  29242  bnj130  29245  bnj153  29251  bnj207  29252  bnj611  29289  bnj864  29293  bnj865  29294  bnj1000  29312  bnj978  29320  bnj1021  29335  bnj1047  29342  bnj1049  29343  bnj1090  29348  bnj1110  29351  bnj1128  29359  bnj1145  29362  bnj1171  29369  bnj1172  29370  bnj1174  29372  bnj1176  29374  bnj1280  29389  sblimNEW7  29568  sbanNEW7  29569  sbhbwAUX7  29607  2sb6NEW7  29610  sbhbOLD7  29760  2sb6rfOLD7  29762  lcvnbtwn3  29826  isat3  30105  cdleme25cv  31155  cdlemefrs29bpre0  31193  cdlemk35  31709
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