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  2358  sb8f  2359  dfsb3  2499  mo4f  2568  2mos  2650  2mosOLD  2651  neor  3025  r19.43  3106  r19.23v  3165  r3al  3176  r19.23t  3234  sbralieOLD  3318  ceqsralt  3465  ralab  3640  ralrab  3641  euind  3671  reu2  3672  rmo4  3677  rmo3f  3681  rmo4f  3682  reuind  3700  2reu5lem3  3704  rmo3  3828  dfdif3OLD  4059  raldifb  4090  elunant  4125  ralin  4190  inssdif0  4315  ssundif  4428  dfif2  4469  pwss  4565  ralsnsg  4615  ralsng  4620  disjsn  4656  snssb  4727  raldifsni  4739  raldifsnb  4740  unissb  4884  intprg  4924  dfiin2g  4974  iunssf  4986  iunss  4988  disjor  5068  dftr2  5195  axrep1  5213  axrep4v  5217  axrep4  5218  axrep6OLD  5222  axpweq  5288  zfpow  5303  axpow2  5304  reusv2lem4  5338  reusv2  5340  elOLD  5386  dffr6  5580  raliunxp  5788  cotrg  6068  idrefALT  6070  cnvsym  6071  asymref2  6074  dffun4  6505  dffun5  6506  dffun7  6519  fununi  6567  fvn0ssdmfun  7020  dff13  7202  dff14b  7219  fnssintima  7310  zfun  7683  uniex2  7685  dfom2  7812  ralxp3f  8080  frpoins3xpg  8083  frpoins3xp3g  8084  xpord2indlem  8090  xpord3inddlem  8097  soseq  8102  fimaxg  9190  fiint  9230  dfsup2  9350  fiming  9406  oemapso  9594  scottexs  9802  scott0s  9803  iscard2  9891  acnnum  9965  dfac9  10050  dfacacn  10055  kmlem4  10067  kmlem12  10075  axpowndlem3  10513  zfcndun  10529  zfcndpow  10530  zfcndac  10533  axgroth5  10738  axgroth6  10742  addsrmo  10987  mulsrmo  10988  infm3  12106  raluz2  12838  nnwos  12856  ralrp  12955  cotr2g  14929  lo1resb  15517  rlimresb  15518  o1resb  15519  modfsummod  15748  isprm4  16644  acsfn1  17618  acsfn2  17620  lublecllem  18315  isirred2  20392  isdomn5  20678  isdomn2OLD  20680  isdomn3  20683  isdomn4r  20687  iunocv  21671  ist1-2  23322  isnrm2  23333  dfconn2  23394  alexsubALTlem3  24024  ismbl  25503  dyadmbllem  25576  ellimc3  25856  dchrelbas2  27214  dchrelbas3  27215  eqcuts2  27792  addsproplem4  27978  addsproplem6  27980  addsprop  27982  negsproplem4  28037  negsproplem6  28039  negsprop  28041  mulsprop  28136  onsis  28280  ons2ind  28281  isch2  31309  choc0  31412  h1dei  31636  mdsl2i  32408  disjorf  32664  bnj1101  34943  bnj1109  34945  bnj1533  35010  bnj580  35071  bnj864  35080  bnj865  35081  bnj978  35107  bnj1049  35132  bnj1090  35137  bnj1145  35151  fineqvpow  35275  vonf1owev  35306  antnestALT  35892  axextprim  35899  axunprim  35901  axpowprim  35902  untuni  35907  3orit  35914  biimpexp  35915  elintfv  35963  dfon2lem8  35986  dfom5b  36108  iineq1i  36394  ixpeq1i  36398  ss-ax8  36423  mh-regprimbi  36743  mh-infprim2bi  36745  rdgeqoa  37700  wl-equsalcom  37882  wl-sb9v  37888  poimirlem25  37980  poimirlem30  37985  tsim1  38465  inxpss  38652  idinxpss  38653  ref5  38654  idinxpssinxp  38658  ineleq  38689  cocossss  38861  cosscnvssid3  38901  trcoss2  38909  redundpbi1  39050  dfeldisj3  39146  qmapeldisjsim  39195  dfantisymrel5  39200  antisymrelres  39201  cvlsupr3  39804  pmapglbx  40229  isltrn2N  40580  cdlemefrs29bpre0  40856  3factsumint2  42475  3factsumint3  42476  3factsumint4  42477  3factsumint  42478  aks4d1p7  42536  aks4d1p8  42540  fphpd  43262  dford4  43475  fnwe2lem2  43497  unielss  43664  safesnsupfilb  43863  faosnf0.11b  43872  ifpidg  43936  ifpid1g  43939  ifpor123g  43953  dfsucon  43968  undmrnresiss  44049  elintima  44098  df3or2  44213  dfhe3  44220  dffrege76  44384  dffrege115  44423  frege131  44439  ntrneikb  44539  ismnuprim  44739  ismnushort  44746  pm14.12  44866  dfvd2an  45027  dfvd3  45036  dfvd3an  45039  uun2221  45257  uun2221p1  45258  uun2221p2  45259  sswfaxreg  45432  modelac8prim  45437  disjinfi  45640  supxrleubrnmptf  45897  fsummulc1f  46019  fsumiunss  46023  fnlimfvre2  46123  limsupreuz  46183  dvmptmulf  46383  dvnmul  46389  dvmptfprodlem  46390  dvnprodlem2  46393  sge0ltfirpmpt2  46872  hoidmv1le  47040  hoidmvle  47046  vonioolem2  47127  smflimlem3  47219  2reu8i  47573  ichexmpl2  47942  setrec2  50182  aacllem  50288