MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1i Structured version   Unicode version

Theorem imbi1i 316
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbi1i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
imbi1i  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2  |-  ( ph  <->  ps )
2 imbi1 314 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  <->  ( ps  ->  ch )
) )
31, 2ax-mp 8 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imbi12i  317  imor  402  ancomsimp  1378  19.43  1615  19.37  1894  dfsb3  2116  sbied  2123  sbor  2140  sbrim  2141  mo4f  2312  2mos  2359  neor  2682  r3al  2755  r19.23t  2812  r19.43  2855  ceqsralt  2971  ralab  3087  ralrab  3088  euind  3113  reu2  3114  rmo4  3119  reuind  3129  2reu5lem3  3133  rmo3  3240  raldifb  3479  unss  3513  ralunb  3520  inssdif0  3687  ssundif  3703  dfif2  3733  pwss  3805  ralsns  3836  disjsn  3860  snss  3918  unissb  4037  intun  4074  intpr  4075  dfiin2g  4116  disjor  4188  dftr2  4296  axrep1  4313  axpweq  4368  zfpow  4370  axpow2  4371  zfun  4694  uniex2  4696  reusv2lem4  4719  reusv2  4721  reusv7OLD  4727  dfom2  4839  raliunxp  5006  asymref2  5243  dffun2  5456  dffun4  5458  dffun5  5459  dffun7  5471  fununi  5509  dff13  5996  fimaxg  7346  fiint  7375  dfsup2  7439  oemapso  7630  scottexs  7803  scott0s  7804  iscard2  7855  acnnum  7925  dfac9  8008  dfacacn  8013  kmlem4  8025  kmlem12  8033  axpowndlem3  8466  zfcndun  8482  zfcndpow  8483  zfcndac  8486  axgroth5  8691  grothpw  8693  axgroth6  8695  infm3  9959  raluz2  10518  nnwos  10536  ralrp  10622  lo1resb  12350  rlimresb  12351  o1resb  12352  isprm4  13081  acsfn1  13878  acsfn2  13880  lubid  14431  isirred2  15798  isdomn2  16351  iunocv  16900  ist1-2  17403  isnrm2  17414  dfcon2  17474  alexsubALTlem3  18072  ismbl  19414  dyadmbllem  19483  ellimc3  19758  dchrelbas2  21013  dchrelbas3  21014  isch2  22718  choc0  22820  h1dei  23044  mdsl2i  23817  xfree2  23940  rmo3f  23974  rmo4fOLD  23975  rmo4f  23976  disjorf  24013  axextprim  25142  axunprim  25144  axpowprim  25145  untuni  25150  3orit  25161  biimpexp  25165  dfon2lem8  25409  predreseq  25446  soseq  25521  dfom5b  25749  raldifsni  26715  fphpd  26858  dford4  27081  fnwe2lem2  27107  islindf4  27266  isdomn3  27481  pm14.12  27579  raldifsnb  28038  dff14b  28055  dfvd2an  28601  dfvd3  28610  dfvd3an  28613  uun2221  28852  uun2221p1  28853  uun2221p2  28854  bnj538  29035  bnj1101  29082  bnj1109  29084  bnj1533  29150  bnj580  29211  bnj864  29220  bnj865  29221  bnj978  29247  bnj1049  29270  bnj1090  29275  bnj1145  29289  sborNEW7  29493  sbrimNEW7  29494  dfsb3NEW7  29566  cvlsupr3  30069  pmapglbx  30493  isltrn2N  30844  cdlemefrs29bpre0  31120
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