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  1425  eximal  1778  nfnbi  1851  19.43  1879  19.37v  1988  19.37  2229  sbrimOLD  2303  sbor  2305  sb8v  2352  sb8f  2353  dfsb3  2496  mo4f  2564  2mos  2646  2mosOLD  2647  neor  3031  r19.43  3119  r19.23v  3180  r3al  3194  r19.23t  3252  sbralie  3355  ceqsralt  3513  ralab  3699  ralabOLD  3700  ralrab  3701  euind  3732  reu2  3733  rmo4  3738  rmo3f  3742  rmo4f  3743  reuind  3761  2reu5lem3  3765  rmo3  3897  dfdif3OLD  4127  raldifb  4158  elunant  4193  inssdif0  4379  ssundif  4493  dfif2  4532  pwss  4627  ralsnsg  4674  ralsng  4679  disjsn  4715  snssb  4786  snssgOLD  4788  raldifsni  4799  raldifsnb  4800  unissb  4943  unissbOLD  4944  intprg  4985  dfiin2g  5036  disjor  5129  dftr2  5266  axrep1  5285  axrep4v  5289  axrep4  5290  axrep6OLD  5294  axpweq  5356  zfpow  5371  axpow2  5372  reusv2lem4  5406  reusv2  5408  el  5447  dffr6  5643  raliunxp  5852  cotrg  6129  cotrgOLD  6130  idrefALT  6133  cnvsym  6134  cnvsymOLD  6135  asymref2  6139  dffun2OLDOLD  6574  dffun4  6578  dffun5  6579  dffun7  6594  fununi  6642  fvn0ssdmfun  7093  dff13  7274  dff14b  7290  fnssintima  7381  zfun  7754  uniex2  7756  dfom2  7888  ralxp3f  8160  frpoins3xpg  8163  frpoins3xp3g  8164  xpord2indlem  8170  xpord3inddlem  8177  soseq  8182  fimaxg  9320  fiint  9363  fiintOLD  9364  dfsup2  9481  fiming  9535  oemapso  9719  scottexs  9924  scott0s  9925  iscard2  10013  acnnum  10089  dfac9  10174  dfacacn  10179  kmlem4  10191  kmlem12  10199  axpowndlem3  10636  zfcndun  10652  zfcndpow  10653  zfcndac  10656  axgroth5  10861  axgroth6  10865  addsrmo  11110  mulsrmo  11111  infm3  12224  raluz2  12936  nnwos  12954  ralrp  13052  cotr2g  15011  lo1resb  15596  rlimresb  15597  o1resb  15598  modfsummod  15826  isprm4  16717  acsfn1  17705  acsfn2  17707  lublecllem  18417  isirred2  20437  isdomn5  20726  isdomn2OLD  20728  isdomn3  20731  isdomn4r  20735  iunocv  21716  ist1-2  23370  isnrm2  23381  dfconn2  23442  alexsubALTlem3  24072  ismbl  25574  dyadmbllem  25647  ellimc3  25928  dchrelbas2  27295  dchrelbas3  27296  eqscut2  27865  addsproplem4  28019  addsproplem6  28021  addsprop  28023  negsproplem4  28077  negsproplem6  28079  negsprop  28081  mulsprop  28170  isch2  31251  choc0  31354  h1dei  31578  mdsl2i  32350  disjorf  32598  bnj1101  34776  bnj1109  34778  bnj1533  34844  bnj580  34905  bnj864  34914  bnj865  34915  bnj978  34941  bnj1049  34966  bnj1090  34971  bnj1145  34985  fineqvpow  35088  axextprim  35680  axunprim  35682  axpowprim  35683  untuni  35688  3orit  35695  biimpexp  35696  elintfv  35745  dfon2lem8  35771  dfom5b  35893  iineq1i  36177  ixpeq1i  36181  ss-ax8  36207  rdgeqoa  37352  wl-equsalcom  37523  wl-sb9v  37529  poimirlem25  37631  poimirlem30  37636  tsim1  38116  ralin  38229  inxpss  38292  idinxpss  38293  ref5  38294  idinxpssinxp  38298  ineleq  38335  cocossss  38417  cosscnvssid3  38457  trcoss2  38465  redundpbi1  38612  dfeldisj3  38700  dfantisymrel5  38743  antisymrelres  38744  cvlsupr3  39325  pmapglbx  39751  isltrn2N  40102  cdlemefrs29bpre0  40378  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  3factsumint  42006  aks4d1p7  42064  aks4d1p8  42068  fphpd  42803  dford4  43017  fnwe2lem2  43039  unielss  43206  safesnsupfilb  43407  faosnf0.11b  43416  ifpidg  43480  ifpid1g  43483  ifpor123g  43497  dfsucon  43512  undmrnresiss  43593  elintima  43642  df3or2  43757  dfhe3  43764  dffrege76  43928  dffrege115  43967  frege131  43983  ntrneikb  44083  ismnuprim  44289  ismnushort  44296  pm14.12  44416  dfvd2an  44579  dfvd3  44588  dfvd3an  44591  uun2221  44810  uun2221p1  44811  uun2221p2  44812  disjinfi  45134  supxrleubrnmptf  45400  fsummulc1f  45526  fsumiunss  45530  fnlimfvre2  45632  limsupreuz  45692  dvmptmulf  45892  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  sge0ltfirpmpt2  46381  hoidmv1le  46549  hoidmvle  46555  vonioolem2  46636  smflimlem3  46728  2reu8i  47062  ichexmpl2  47394  setrec2  48925  aacllem  49031