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 205

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 206

This theorem is referenced by:  ancomst  465  imor  851  ifpnOLD  1073  eximal  1784  nfnbi  1857  19.43  1885  19.37v  1995  19.37  2225  sbrimOLD  2301  sbor  2303  sb8v  2348  sb8f  2349  dfsb3  2492  mo4f  2560  2mos  2644  neor  3033  r19.43  3121  r19.23v  3181  r3al  3195  r19.23t  3251  ceqsralt  3504  ralab  3683  ralabOLD  3684  ralrab  3685  euind  3716  reu2  3717  rmo4  3722  rmo3f  3726  rmo4f  3727  reuind  3745  2reu5lem3  3749  rmo3  3879  dfdif3  4110  raldifb  4140  elunant  4174  inssdif0  4365  ssundif  4481  dfif2  4524  pwss  4619  ralsnsg  4665  ralsng  4670  disjsn  4708  snssb  4779  snssgOLD  4781  raldifsni  4791  raldifsnb  4792  unissb  4936  unissbOLD  4937  intprg  4978  intprOLD  4980  dfiin2g  5028  disjor  5121  dftr2  5260  axrep1  5279  axrep6  5285  axpweq  5341  zfpow  5357  axpow2  5358  reusv2lem4  5392  reusv2  5394  el  5430  dffr6  5627  raliunxp  5831  cotrg  6097  cotrgOLD  6098  idrefALT  6101  cnvsym  6102  cnvsymOLD  6103  asymref2  6107  dffun2OLDOLD  6544  dffun4  6548  dffun5  6549  dffun7  6564  fununi  6612  fvn0ssdmfun  7061  dff13  7238  dff14b  7254  fnssintima  7343  zfun  7709  uniex2  7711  dfom2  7840  ralxp3f  8105  frpoins3xpg  8108  frpoins3xp3g  8109  xpord2indlem  8115  xpord3inddlem  8122  soseq  8127  fimaxg  9273  fiint  9307  dfsup2  9421  fiming  9475  oemapso  9659  scottexs  9864  scott0s  9865  iscard2  9953  acnnum  10029  dfac9  10113  dfacacn  10118  kmlem4  10130  kmlem12  10138  axpowndlem3  10576  zfcndun  10592  zfcndpow  10593  zfcndac  10596  axgroth5  10801  axgroth6  10805  addsrmo  11050  mulsrmo  11051  infm3  12155  raluz2  12863  nnwos  12881  ralrp  12976  cotr2g  14905  lo1resb  15490  rlimresb  15491  o1resb  15492  modfsummod  15722  isprm4  16603  acsfn1  17587  acsfn2  17589  lublecllem  18295  isirred2  20185  isdomn2  20851  iunocv  21167  ist1-2  22780  isnrm2  22791  dfconn2  22852  alexsubALTlem3  23482  ismbl  24972  dyadmbllem  25045  ellimc3  25325  dchrelbas2  26667  dchrelbas3  26668  eqscut2  27233  addsproplem4  27372  addsproplem6  27374  addsprop  27376  negsproplem4  27421  negsproplem6  27423  negsprop  27425  mulsprop  27499  isch2  30339  choc0  30442  h1dei  30666  mdsl2i  31438  disjorf  31675  bnj1101  33626  bnj1109  33628  bnj1533  33694  bnj580  33755  bnj864  33764  bnj865  33765  bnj978  33791  bnj1049  33816  bnj1090  33821  bnj1145  33835  fineqvpow  33927  axextprim  34500  axunprim  34502  axpowprim  34503  untuni  34508  3orit  34515  biimpexp  34516  elintfv  34566  dfon2lem8  34592  dfom5b  34714  rdgeqoa  36055  wl-equsalcom  36215  poimirlem25  36317  poimirlem30  36322  tsim1  36803  ralin  36920  inxpss  36985  idinxpss  36986  ref5  36987  idinxpssinxp  36991  ineleq  37028  cocossss  37111  cosscnvssid3  37151  trcoss2  37159  redundpbi1  37306  dfeldisj3  37394  dfantisymrel5  37437  antisymrelres  37438  cvlsupr3  38019  pmapglbx  38445  isltrn2N  38796  cdlemefrs29bpre0  39072  3factsumint2  40692  3factsumint3  40693  3factsumint4  40694  3factsumint  40695  aks4d1p7  40753  aks4d1p8  40757  isdomn5  40836  fphpd  41325  dford4  41539  fnwe2lem2  41564  isdomn3  41717  unielss  41738  safesnsupfilb  41940  faosnf0.11b  41949  ifpidg  42013  ifpid1g  42016  ifpor123g  42030  dfsucon  42045  undmrnresiss  42126  elintima  42175  df3or2  42290  dfhe3  42297  dffrege76  42461  dffrege115  42500  frege131  42516  ntrneikb  42616  ismnuprim  42824  ismnushort  42831  pm14.12  42951  dfvd2an  43114  dfvd3  43123  dfvd3an  43126  uun2221  43345  uun2221p1  43346  uun2221p2  43347  disjinfi  43662  supxrleubrnmptf  43934  fsummulc1f  44060  fsumiunss  44064  fnlimfvre2  44166  limsupreuz  44226  limsupvaluz2  44227  dvmptmulf  44426  dvnmul  44432  dvmptfprodlem  44433  dvnprodlem2  44436  sge0ltfirpmpt2  44915  hoidmv1le  45083  hoidmvle  45089  vonioolem2  45170  smflimlem3  45262  2reu8i  45593  ichexmpl2  45910  setrec2  47388  aacllem  47496