Theorem imbi1i 353

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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi1i	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		imbi1 351	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ancomst  468  imor  850  ifpnOLD  1070  eximal  1784  19.43  1883  19.37v  1998  19.37  2232  sbrim  2309  sbor  2312  dfsb3  2512  mo4f  2585  2mos  2670  neor  3042  r3al  3131  r19.23v  3203  r19.23t  3237  r19.43  3269  ceqsralt  3444  ralab  3609  ralrab  3610  euind  3640  reu2  3641  rmo4  3646  rmo3f  3650  rmo4f  3651  reuind  3669  2reu5lem3  3673  rmo3  3797  dfdif3  4022  raldifb  4052  elunant  4085  inssdif0  4270  ssundif  4384  dfif2  4425  pwss  4522  ralsnsg  4568  disjsn  4607  snssg  4678  raldifsni  4688  raldifsnb  4689  unissb  4835  intprg  4874  intprOLD  4876  dfiin2g  4924  disjor  5015  dftr2  5143  axrep1  5160  axrep6  5166  axpweq  5236  zfpow  5238  axpow2  5239  reusv2lem4  5273  reusv2  5275  raliunxp  5684  idrefALT  5949  asymref2  5953  dffun2  6349  dffun4  6351  dffun5  6352  dffun7  6366  fununi  6414  fvn0ssdmfun  6838  dff13  7010  dff14b  7026  zfun  7465  uniex2  7467  dfom2  7586  fimaxg  8803  fiint  8833  dfsup2  8946  fiming  9000  oemapso  9183  scottexs  9354  scott0s  9355  iscard2  9443  acnnum  9517  dfac9  9601  dfacacn  9606  kmlem4  9618  kmlem12  9626  axpowndlem3  10064  zfcndun  10080  zfcndpow  10081  zfcndac  10084  axgroth5  10289  axgroth6  10293  addsrmo  10538  mulsrmo  10539  infm3  11641  raluz2  12342  nnwos  12360  ralrp  12455  cotr2g  14388  lo1resb  14974  rlimresb  14975  o1resb  14976  modfsummod  15202  isprm4  16085  acsfn1  16995  acsfn2  16997  lublecllem  17669  isirred2  19527  isdomn2  20145  iunocv  20451  ist1-2  22052  isnrm2  22063  dfconn2  22124  alexsubALTlem3  22754  ismbl  24231  dyadmbllem  24304  ellimc3  24583  dchrelbas2  25925  dchrelbas3  25926  isch2  29110  choc0  29213  h1dei  29437  mdsl2i  30209  disjorf  30445  bnj1101  32288  bnj1109  32290  bnj1533  32356  bnj580  32417  bnj864  32426  bnj865  32427  bnj978  32453  bnj1049  32478  bnj1090  32483  bnj1145  32497  axextprim  33162  axunprim  33164  axpowprim  33165  untuni  33170  3orit  33180  biimpexp  33181  fnssintima  33198  ralxp3f  33208  elintfv  33258  dfon2lem8  33286  frpoins3xpg  33336  frpoins3xp3g  33337  xpord2ind  33353  xpord3ind  33359  soseq  33362  eqscut2  33587  no3indslem  33689  dfom5b  33789  rdgeqoa  35093  wl-equsalcom  35253  wl-dfralflem  35309  poimirlem25  35388  poimirlem30  35393  tsim1  35874  inxpss  36035  idinxpss  36036  idinxpssinxp  36040  ineleq  36074  cocossss  36147  cosscnvssid3  36182  trcoss2  36190  redundpbi1  36332  dfeldisj3  36418  cvlsupr3  36946  pmapglbx  37371  isltrn2N  37722  cdlemefrs29bpre0  37998  3factsumint2  39615  3factsumint3  39616  3factsumint4  39617  3factsumint  39618  fphpd  40158  dford4  40371  fnwe2lem2  40396  isdomn3  40549  ifpidg  40600  ifpid1g  40603  ifpor123g  40617  dfsucon  40632  undmrnresiss  40705  elintima  40755  df3or2  40870  dfhe3  40877  dffrege76  41041  dffrege115  41080  frege131  41096  ntrneikb  41198  ismnuprim  41403  pm14.12  41526  dfvd2an  41689  dfvd3  41698  dfvd3an  41701  uun2221  41920  uun2221p1  41921  uun2221p2  41922  disjinfi  42218  supxrleubrnmptf  42484  fsummulc1f  42606  fsumiunss  42611  fnlimfvre2  42713  limsupreuz  42773  limsupvaluz2  42774  dvmptmulf  42973  dvnmul  42979  dvmptfprodlem  42980  dvnprodlem2  42983  sge0ltfirpmpt2  43459  hoidmv1le  43627  hoidmvle  43633  vonioolem2  43714  smflimlem3  43800  2reu8i  44065  ichexmpl2  44383  setrec2  45689  aacllem  45793