Theorem imbi1i 323

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-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

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 |- ( ph <-> ps )
2		imbi1 321	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

Syntax hints:   -> wi 4   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  imor  410  ancomst  450  ifpn  1390  eximal  1620  19.43  1698  19.37v  1773  19.37  1971  dfsb3  2117  sbrim  2139  sbor  2141  mo4f  2334  2mos  2372  neor  2778  r3al  2834  r3alOLD  2892  r19.23t  2932  r19.23v  2934  r19.43  3010  ceqsralt  3130  ralab  3257  ralrab  3258  euind  3283  reu2  3284  rmo4  3289  reuind  3300  2reu5lem3  3304  rmo3  3415  raldifb  3630  unss  3664  ralunb  3671  inssdif0  3883  ssundif  3899  dfif2  3931  pwss  4014  ralsnsg  4048  disjsn  4076  snss  4140  raldifsni  4146  raldifsnb  4147  unissb  4266  intun  4304  intpr  4305  dfiin2g  4348  disjor  4424  dftr2  4534  axrep1  4551  axpweq  4614  zfpow  4616  axpow2  4617  reusv2lem4  4641  reusv2  4643  reusv7OLD  4649  raliunxp  5131  asymref2  5372  dffun2  5580  dffun4  5582  dffun5  5583  dffun7  5596  fununi  5636  fvn0ssdmfun  5998  dff13  6141  dff14b  6153  zfun  6566  uniex2  6568  dfom2  6675  fimaxg  7759  fiint  7789  dfsup2  7894  oemapso  8092  scottexs  8296  scott0s  8297  iscard2  8348  acnnum  8424  dfac9  8507  dfacacn  8512  kmlem4  8524  kmlem12  8532  axpowndlem3  8965  zfcndun  8982  zfcndpow  8983  zfcndac  8986  axgroth5  9191  grothpw  9193  axgroth6  9195  addsrmo  9439  mulsrmo  9440  infm3  10497  raluz2  11131  nnwos  11150  ralrp  11240  cotr2g  12894  lo1resb  13469  rlimresb  13470  o1resb  13471  modfsummod  13690  isprm4  14311  acsfn1  15150  acsfn2  15152  lublecllem  15817  isirred2  17545  isdomn2  18143  iunocv  18885  ist1-2  20015  isnrm2  20026  dfcon2  20086  alexsubALTlem3  20715  ismbl  22103  dyadmbllem  22174  ellimc3  22449  dchrelbas2  23710  dchrelbas3  23711  isch2  26339  choc0  26442  h1dei  26666  mdsl2i  27439  rmo3f  27592  rmo4fOLD  27593  rmo4f  27594  disjorf  27650  axextprim  29314  axunprim  29316  axpowprim  29317  untuni  29322  3orit  29333  biimpexp  29334  dfon2lem8  29462  predreseq  29499  soseq  29574  dfom5b  29790  wl-equsalcom  30235  tsim1  30777  fphpd  30989  dford4  31210  fnwe2lem2  31236  isdomn3  31405  pm14.12  31569  fsummulc1f  31808  dvmptmulf  31973  dvnmul  31979  dvmptfprodlem  31980  dvnprodlem2  31983  aacllem  33604  dfvd2an  33753  dfvd3  33762  dfvd3an  33765  uun2221  34004  uun2221p1  34005  uun2221p2  34006  bnj538OLD  34198  bnj1101  34244  bnj1109  34246  bnj1533  34311  bnj580  34372  bnj864  34381  bnj865  34382  bnj978  34408  bnj1049  34431  bnj1090  34436  bnj1145  34450  bj-axrep1  34775  bj-zfpow  34782  cvlsupr3  35466  pmapglbx  35890  isltrn2N  36241  cdlemefrs29bpre0  36519  ifpidg  38105  ifpid1g  38106  ifpor123g  38132  elintima  38177  dfhe3  38249  lem1frege76a  38417