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  853  3jaob  1428  eximal  1782  nfnbi  1855  19.43  1882  19.37v  1997  19.37  2233  sbor  2306  sb8v  2351  sb8f  2352  dfsb3  2493  mo4f  2561  2mos  2643  2mosOLD  2644  neor  3018  r19.43  3102  r19.23v  3162  r3al  3176  r19.23t  3234  sbralieOLD  3330  ceqsralt  3485  ralab  3667  ralrab  3668  euind  3698  reu2  3699  rmo4  3704  rmo3f  3708  rmo4f  3709  reuind  3727  2reu5lem3  3731  rmo3  3855  dfdif3OLD  4084  raldifb  4115  elunant  4150  ralin  4215  inssdif0  4340  ssundif  4454  dfif2  4493  pwss  4589  ralsnsg  4637  ralsng  4642  disjsn  4678  snssb  4749  snssgOLD  4751  raldifsni  4762  raldifsnb  4763  unissb  4906  unissbOLD  4907  intprg  4948  dfiin2g  4999  disjor  5092  dftr2  5219  axrep1  5238  axrep4v  5242  axrep4  5243  axrep6OLD  5247  axpweq  5309  zfpow  5324  axpow2  5325  reusv2lem4  5359  reusv2  5361  el  5400  dffr6  5597  raliunxp  5806  cotrg  6083  cotrgOLD  6084  idrefALT  6087  cnvsym  6088  cnvsymOLD  6089  asymref2  6093  dffun2OLDOLD  6526  dffun4  6530  dffun5  6531  dffun7  6546  fununi  6594  fvn0ssdmfun  7049  dff13  7232  dff14b  7249  fnssintima  7340  zfun  7715  uniex2  7717  dfom2  7847  ralxp3f  8119  frpoins3xpg  8122  frpoins3xp3g  8123  xpord2indlem  8129  xpord3inddlem  8136  soseq  8141  fimaxg  9241  fiint  9284  fiintOLD  9285  dfsup2  9402  fiming  9458  oemapso  9642  scottexs  9847  scott0s  9848  iscard2  9936  acnnum  10012  dfac9  10097  dfacacn  10102  kmlem4  10114  kmlem12  10122  axpowndlem3  10559  zfcndun  10575  zfcndpow  10576  zfcndac  10579  axgroth5  10784  axgroth6  10788  addsrmo  11033  mulsrmo  11034  infm3  12149  raluz2  12863  nnwos  12881  ralrp  12980  cotr2g  14949  lo1resb  15537  rlimresb  15538  o1resb  15539  modfsummod  15767  isprm4  16661  acsfn1  17629  acsfn2  17631  lublecllem  18326  isirred2  20337  isdomn5  20626  isdomn2OLD  20628  isdomn3  20631  isdomn4r  20635  iunocv  21597  ist1-2  23241  isnrm2  23252  dfconn2  23313  alexsubALTlem3  23943  ismbl  25434  dyadmbllem  25507  ellimc3  25787  dchrelbas2  27155  dchrelbas3  27156  eqscut2  27725  addsproplem4  27886  addsproplem6  27888  addsprop  27890  negsproplem4  27944  negsproplem6  27946  negsprop  27948  mulsprop  28040  onsis  28179  isch2  31159  choc0  31262  h1dei  31486  mdsl2i  32258  disjorf  32515  bnj1101  34781  bnj1109  34783  bnj1533  34849  bnj580  34910  bnj864  34919  bnj865  34920  bnj978  34946  bnj1049  34971  bnj1090  34976  bnj1145  34990  fineqvpow  35093  vonf1owev  35102  antnestALT  35688  axextprim  35695  axunprim  35697  axpowprim  35698  untuni  35703  3orit  35710  biimpexp  35711  elintfv  35759  dfon2lem8  35785  dfom5b  35907  iineq1i  36191  ixpeq1i  36195  ss-ax8  36220  rdgeqoa  37365  wl-equsalcom  37538  wl-sb9v  37544  poimirlem25  37646  poimirlem30  37651  tsim1  38131  inxpss  38306  idinxpss  38307  ref5  38308  idinxpssinxp  38312  ineleq  38343  cocossss  38434  cosscnvssid3  38474  trcoss2  38482  redundpbi1  38629  dfeldisj3  38718  dfantisymrel5  38761  antisymrelres  38762  cvlsupr3  39344  pmapglbx  39770  isltrn2N  40121  cdlemefrs29bpre0  40397  3factsumint2  42017  3factsumint3  42018  3factsumint4  42019  3factsumint  42020  aks4d1p7  42078  aks4d1p8  42082  fphpd  42811  dford4  43025  fnwe2lem2  43047  unielss  43214  safesnsupfilb  43414  faosnf0.11b  43423  ifpidg  43487  ifpid1g  43490  ifpor123g  43504  dfsucon  43519  undmrnresiss  43600  elintima  43649  df3or2  43764  dfhe3  43771  dffrege76  43935  dffrege115  43974  frege131  43990  ntrneikb  44090  ismnuprim  44290  ismnushort  44297  pm14.12  44417  dfvd2an  44579  dfvd3  44588  dfvd3an  44591  uun2221  44809  uun2221p1  44810  uun2221p2  44811  sswfaxreg  44984  modelac8prim  44989  disjinfi  45193  supxrleubrnmptf  45454  fsummulc1f  45576  fsumiunss  45580  fnlimfvre2  45682  limsupreuz  45742  dvmptmulf  45942  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem2  45952  sge0ltfirpmpt2  46431  hoidmv1le  46599  hoidmvle  46605  vonioolem2  46686  smflimlem3  46778  2reu8i  47118  ichexmpl2  47475  setrec2  49688  aacllem  49794