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

Theorem imbi1i 315
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 313 . 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 176
This theorem is referenced by:  imbi12i  316  imor  401  ancomsimp  1359  19.43  1592  19.37  1809  dfsb3  1996  sbor  2006  sbrim  2007  mo4f  2175  2mos  2222  neor  2530  r3al  2600  r19.23t  2657  r19.43  2695  ceqsralt  2811  ralab  2926  ralrab  2927  euind  2952  reu2  2953  rmo4  2958  reuind  2968  2reu5lem3  2972  rmo3  3078  unss  3349  ralunb  3356  inssdif0  3521  ssundif  3537  dfif2  3567  pwss  3639  ralsns  3670  disjsn  3693  snss  3748  unissb  3857  intun  3894  intpr  3895  dfiin2g  3936  disjor  4007  dftr2  4115  axrep1  4132  axpweq  4187  zfpow  4189  axpow2  4190  zfun  4513  uniex2  4515  reusv2lem4  4538  reusv2  4540  reusv7OLD  4546  dfom2  4658  raliunxp  4825  asymref2  5060  dffun2  5265  dffun4  5267  dffun5  5268  dffun7  5280  fununi  5316  dff13  5783  fimaxg  7104  fiint  7133  dfsup2  7195  oemapso  7384  scottexs  7557  scott0s  7558  iscard2  7609  acnnum  7679  dfac9  7762  dfacacn  7767  kmlem4  7779  kmlem12  7787  axpowndlem3  8221  zfcndun  8237  zfcndpow  8238  zfcndac  8241  axgroth5  8446  grothpw  8448  axgroth6  8450  infm3  9713  raluz2  10268  nnwos  10286  ralrp  10372  lo1resb  12038  rlimresb  12039  o1resb  12040  isprm4  12768  acsfn1  13563  acsfn2  13565  lubid  14116  isirred2  15483  isdomn2  16040  iunocv  16581  ist1-2  17075  isnrm2  17086  dfcon2  17145  alexsubALTlem3  17743  ismbl  18885  dyadmbllem  18954  ellimc3  19229  dchrelbas2  20476  dchrelbas3  20477  isch2  21803  choc0  21905  h1dei  22129  mdsl2i  22902  xfree2  23025  rmo3f  23178  rmo4fOLD  23179  rmo4f  23180  difprsn2  23191  disjorf  23356  esumpcvgval  23446  esumcvg  23454  axextprim  24047  axunprim  24049  axpowprim  24050  untuni  24055  3orit  24066  biimpexp  24070  dfon2lem8  24146  predreseq  24179  soseq  24254  dfom5b  24452  fates  24955  domrngref  25060  trooo  25394  vecval1b  25451  prcnt  25551  isconcl5a  26101  isconcl5ab  26102  raldifsni  26753  fphpd  26899  dford4  27122  fnwe2lem2  27148  islindf4  27308  isdomn3  27523  pm14.12  27621  dfvd2an  28351  dfvd3  28360  dfvd3an  28363  uun2221  28588  uun2221p1  28589  uun2221p2  28590  bnj538  28769  bnj1101  28816  bnj1109  28818  bnj1533  28884  bnj580  28945  bnj864  28954  bnj865  28955  bnj978  28981  bnj1049  29004  bnj1090  29009  bnj1145  29023  a12study8  29119  a12study9  29120  a12peros  29121  a12lem2  29131  cvlsupr3  29534  pmapglbx  29958  isltrn2N  30309  cdleme0moN  30414  cdlemefrs29bpre0  30585
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