Theorem imbi1i 349

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 347	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ancomst  464  imor  854  3jaob  1429  eximal  1784  nfnbi  1857  19.43  1884  19.37v  1999  19.37  2240  sbor  2313  sb8v  2357  sb8f  2358  dfsb3  2498  mo4f  2567  2mos  2649  2mosOLD  2650  neor  3024  r19.43  3105  r19.23v  3164  r3al  3175  r19.23t  3233  sbralieOLD  3317  ceqsralt  3464  ralab  3639  ralrab  3640  euind  3670  reu2  3671  rmo4  3676  rmo3f  3680  rmo4f  3681  reuind  3699  2reu5lem3  3703  rmo3  3827  dfdif3OLD  4058  raldifb  4089  elunant  4124  ralin  4189  inssdif0  4314  ssundif  4427  dfif2  4468  pwss  4564  ralsnsg  4614  ralsng  4619  disjsn  4655  snssb  4726  raldifsni  4740  raldifsnb  4741  unissb  4883  intprg  4923  dfiin2g  4973  iunssf  4985  iunss  4987  disjor  5067  dftr2  5194  axrep1  5213  axrep4v  5217  axrep4  5218  axrep6OLD  5222  axpweq  5292  zfpow  5308  axpow2  5309  reusv2lem4  5343  reusv2  5345  elOLD  5391  dffr6  5587  raliunxp  5794  cotrg  6074  idrefALT  6076  cnvsym  6077  asymref2  6080  dffun4  6511  dffun5  6512  dffun7  6525  fununi  6573  fvn0ssdmfun  7026  dff13  7209  dff14b  7226  fnssintima  7317  zfun  7690  uniex2  7692  dfom2  7819  ralxp3f  8087  frpoins3xpg  8090  frpoins3xp3g  8091  xpord2indlem  8097  xpord3inddlem  8104  soseq  8109  fimaxg  9197  fiint  9237  dfsup2  9357  fiming  9413  oemapso  9603  scottexs  9811  scott0s  9812  iscard2  9900  acnnum  9974  dfac9  10059  dfacacn  10064  kmlem4  10076  kmlem12  10084  axpowndlem3  10522  zfcndun  10538  zfcndpow  10539  zfcndac  10542  axgroth5  10747  axgroth6  10751  addsrmo  10996  mulsrmo  10997  infm3  12115  raluz2  12847  nnwos  12865  ralrp  12964  cotr2g  14938  lo1resb  15526  rlimresb  15527  o1resb  15528  modfsummod  15757  isprm4  16653  acsfn1  17627  acsfn2  17629  lublecllem  18324  isirred2  20401  isdomn5  20687  isdomn2OLD  20689  isdomn3  20692  isdomn4r  20696  iunocv  21661  ist1-2  23312  isnrm2  23323  dfconn2  23384  alexsubALTlem3  24014  ismbl  25493  dyadmbllem  25566  ellimc3  25846  dchrelbas2  27200  dchrelbas3  27201  eqcuts2  27778  addsproplem4  27964  addsproplem6  27966  addsprop  27968  negsproplem4  28023  negsproplem6  28025  negsprop  28027  mulsprop  28122  onsis  28266  ons2ind  28267  isch2  31294  choc0  31397  h1dei  31621  mdsl2i  32393  disjorf  32649  bnj1101  34927  bnj1109  34929  bnj1533  34994  bnj580  35055  bnj864  35064  bnj865  35065  bnj978  35091  bnj1049  35116  bnj1090  35121  bnj1145  35135  fineqvpow  35259  vonf1owev  35290  antnestALT  35876  axextprim  35883  axunprim  35885  axpowprim  35886  untuni  35891  3orit  35898  biimpexp  35899  elintfv  35947  dfon2lem8  35970  dfom5b  36092  iineq1i  36378  ixpeq1i  36382  ss-ax8  36407  mh-regprimbi  36727  mh-infprim2bi  36729  rdgeqoa  37686  wl-equsalcom  37868  wl-sb9v  37874  poimirlem25  37966  poimirlem30  37971  tsim1  38451  inxpss  38638  idinxpss  38639  ref5  38640  idinxpssinxp  38644  ineleq  38675  cocossss  38847  cosscnvssid3  38887  trcoss2  38895  redundpbi1  39036  dfeldisj3  39132  qmapeldisjsim  39181  dfantisymrel5  39186  antisymrelres  39187  cvlsupr3  39790  pmapglbx  40215  isltrn2N  40566  cdlemefrs29bpre0  40842  3factsumint2  42461  3factsumint3  42462  3factsumint4  42463  3factsumint  42464  aks4d1p7  42522  aks4d1p8  42526  fphpd  43244  dford4  43457  fnwe2lem2  43479  unielss  43646  safesnsupfilb  43845  faosnf0.11b  43854  ifpidg  43918  ifpid1g  43921  ifpor123g  43935  dfsucon  43950  undmrnresiss  44031  elintima  44080  df3or2  44195  dfhe3  44202  dffrege76  44366  dffrege115  44405  frege131  44421  ntrneikb  44521  ismnuprim  44721  ismnushort  44728  pm14.12  44848  dfvd2an  45009  dfvd3  45018  dfvd3an  45021  uun2221  45239  uun2221p1  45240  uun2221p2  45241  sswfaxreg  45414  modelac8prim  45419  disjinfi  45622  supxrleubrnmptf  45879  fsummulc1f  46001  fsumiunss  46005  fnlimfvre2  46105  limsupreuz  46165  dvmptmulf  46365  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem2  46375  sge0ltfirpmpt2  46854  hoidmv1le  47022  hoidmvle  47028  vonioolem2  47109  smflimlem3  47201  2reu8i  47561  ichexmpl2  47930  setrec2  50170  aacllem  50276