Theorem imbi1i 339

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 337	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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

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 197

This theorem is referenced by:  imor  428  ancomst  468  ifpn  1022  eximal  1707  19.43  1810  19.37v  1910  19.37  2100  dfsb3  2374  sbrim  2396  sbor  2398  mo4f  2516  2mos  2552  neor  2885  r3al  2940  r19.23t  3021  r19.23v  3023  r19.43  3093  ceqsralt  3229  ralab  3367  ralrab  3368  euind  3393  reu2  3394  rmo4  3399  reuind  3411  2reu5lem3  3415  rmo3  3528  raldifb  3750  unss  3787  ralunb  3794  inssdif0  3947  dfnf5  3952  ssundif  4052  dfif2  4088  pwss  4175  ralsnsg  4216  disjsn  4246  snss  4316  raldifsni  4324  raldifsnb  4325  unissb  4469  intun  4509  intpr  4510  dfiin2g  4553  disjor  4634  dftr2  4754  axrep1  4772  axpweq  4842  zfpow  4844  axpow2  4845  reusv2lem4  4872  reusv2  4874  raliunxp  5261  asymref2  5513  dffun2  5898  dffun4  5900  dffun5  5901  dffun7  5915  fununi  5964  fvn0ssdmfun  6350  dff13  6512  dff14b  6528  zfun  6950  uniex2  6952  dfom2  7067  fimaxg  8207  fiint  8237  dfsup2  8350  fiming  8404  oemapso  8579  scottexs  8750  scott0s  8751  iscard2  8802  acnnum  8875  dfac9  8958  dfacacn  8963  kmlem4  8975  kmlem12  8983  axpowndlem3  9421  zfcndun  9437  zfcndpow  9438  zfcndac  9441  axgroth5  9646  grothpw  9648  axgroth6  9650  addsrmo  9894  mulsrmo  9895  infm3  10982  raluz2  11737  nnwos  11755  ralrp  11852  cotr2g  13715  lo1resb  14295  rlimresb  14296  o1resb  14297  modfsummod  14526  isprm4  15397  acsfn1  16322  acsfn2  16324  lublecllem  16988  isirred2  18701  isdomn2  19299  iunocv  20025  ist1-2  21151  isnrm2  21162  dfconn2  21222  alexsubALTlem3  21853  ismbl  23294  dyadmbllem  23367  ellimc3  23643  dchrelbas2  24962  dchrelbas3  24963  isch2  28080  choc0  28185  h1dei  28409  mdsl2i  29181  rmo3f  29335  rmo4fOLD  29336  rmo4f  29337  disjorf  29392  bnj538OLD  30810  bnj1101  30855  bnj1109  30857  bnj1533  30922  bnj580  30983  bnj864  30992  bnj865  30993  bnj978  31019  bnj1049  31042  bnj1090  31047  bnj1145  31061  axextprim  31578  axunprim  31580  axpowprim  31581  untuni  31586  3orit  31596  biimpexp  31597  elintfv  31662  dfon2lem8  31695  soseq  31751  dfom5b  32019  bj-axrep1  32788  bj-zfpow  32795  bj-raldifsn  33054  rdgeqoa  33218  wl-equsalcom  33328  poimirlem25  33434  poimirlem30  33439  tsim1  33937  inxpss  34082  idinxpss  34083  idinxpssinxp  34087  ineleq  34119  cvlsupr3  34631  pmapglbx  35055  isltrn2N  35406  cdlemefrs29bpre0  35684  fphpd  37380  dford4  37596  fnwe2lem2  37621  isdomn3  37782  ifpidg  37836  ifpid1g  37839  ifpor123g  37853  undmrnresiss  37910  elintima  37945  df3or2  38060  dfhe3  38069  dffrege76  38233  dffrege115  38272  frege131  38288  ntrneikb  38392  ntrneixb  38393  pm14.12  38622  dfvd2an  38798  dfvd3  38807  dfvd3an  38810  uun2221  39040  uun2221p1  39041  uun2221p2  39042  disjinfi  39380  supxrleubrnmptf  39680  fsummulc1f  39802  fsumiunss  39807  fnlimfvre2  39909  limsupreuz  39969  limsupvaluz2  39970  dvmptmulf  40152  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem2  40162  sge0ltfirpmpt2  40643  hoidmv1le  40808  hoidmvle  40814  vonioolem2  40895  smflimlem3  40981  setrec2  42442  aacllem  42547