Theorem imbi1i 352

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ancomst  469  imor  866  3jaob  1451  eximal  1809  nfnbi  1882  19.43  1909  19.37v  2024  19.37  2274  sbor  2347  sb8v  2391  sb8f  2392  dfsb3  2532  mo4f  2601  2mos  2683  neor  3056  r19.43  3139  r19.23v  3198  r3al  3209  r19.23t  3267  sbralieOLD  3351  ceqsralt  3497  ralab  3665  ralrab  3666  euind  3696  reu2  3697  rmo4  3702  rmo3f  3706  rmo4f  3707  reuind  3725  2reu5lem3  3729  rmo3  3851  dfdif3OLD  4081  raldifb  4111  elunant  4145  ralin  4210  inssdif0  4336  ssundif  4450  dfif2  4491  pwss  4588  ralsnsg  4638  ralsng  4643  disjsn  4679  snssb  4750  raldifsni  4764  raldifsnb  4765  unissb  4907  intprg  4947  dfiin2g  4996  iunssf  5008  iunss  5010  disjor  5092  dftr2  5221  axrep1  5240  axrep4v  5244  axrep4  5245  axrep6OLD  5249  axpweq  5319  zfpow  5335  axpow2  5336  reusv2lem4  5370  reusv2  5372  elOLD  5418  dffr6  5615  raliunxp  5823  cotrg  6109  idrefALT  6111  cnvsym  6112  asymref2  6115  dffun4  6547  dffun5  6548  dffun7  6561  fununi  6609  fvn0ssdmfun  7067  dff13  7250  dff14b  7267  fnssintima  7358  zfun  7731  uniex2  7733  dfom2  7860  ralxp3f  8129  frpoins3xpg  8132  frpoins3xp3g  8133  xpord2indlem  8139  xpord3inddlem  8146  soseq  8151  fimaxg  9243  fiint  9282  dfsup2  9400  fiming  9456  oemapso  9647  scottexs  9857  scott0s  9858  iscard2  9958  acnnum  10032  dfac9  10116  dfacacn  10121  kmlem4  10133  kmlem12  10141  axpowndlem3  10580  zfcndun  10596  zfcndpow  10597  zfcndac  10600  axgroth5  10805  axgroth6  10809  addsrmo  11054  mulsrmo  11055  infm3  12170  raluz2  12917  nnwos  12935  ralrp  13034  cotr2g  15009  lo1resb  15611  rlimresb  15612  o1resb  15613  modfsummod  15842  isprm4  16738  acsfn1  17713  acsfn2  17715  lublecllem  18410  isirred2  20499  isdomn5  20791  isdomn3  20795  isdomn4r  20799  iunocv  21796  ist1-2  23469  isnrm2  23480  dfconn2  23541  alexsubALTlem3  24171  ismbl  25650  dyadmbllem  25723  ellimc3  26003  dchrelbas2  27363  dchrelbas3  27364  eqcuts2  27941  addsproplem4  28127  addsproplem6  28129  addsprop  28131  negsproplem4  28186  negsproplem6  28188  negsprop  28190  mulsprop  28285  onsis  28429  ons2ind  28430  isch2  31512  choc0  31615  h1dei  31839  mdsl2i  32611  disjorf  32861  bnj1101  35114  bnj1109  35116  bnj1533  35181  bnj580  35242  bnj864  35251  bnj865  35252  bnj978  35278  bnj1049  35303  bnj1090  35308  bnj1145  35322  fineqvpow  35447  axpowg  35478  vonf1wev  35487  vonf1owevOLD  35489  antnestALT  36081  axextprim  36088  axunprim  36090  axpowprim  36091  untuni  36096  3orit  36103  biimpexp  36104  elintfv  36152  dfon2lem8  36175  dfom5b  36297  iineq1i  36593  ixpeq1i  36597  ss-ax8  36622  mh-regprimbi  36941  mh-infprim2bi  36943  rdgeqoa  37899  wl-equsalcom  38081  wl-sb9v  38087  poimirlem25  38179  poimirlem30  38184  tsim1  38664  inxpss  38851  idinxpss  38852  ref5  38853  idinxpssinxp  38857  ineleq  38888  cocossss  39060  cosscnvssid3  39100  trcoss2  39108  redundpbi1  39249  dfeldisj3  39345  qmapeldisjsim  39394  dfantisymrel5  39399  antisymrelres  39400  cvlsupr3  40003  pmapglbx  40428  isltrn2N  40779  cdlemefrs29bpre0  41055  3factsumint2  42674  3factsumint3  42675  3factsumint4  42676  3factsumint  42677  aks4d1p7  42735  aks4d1p8  42739  fphpd  43430  dford4  43643  fnwe2lem2  43665  unielss  43832  safesnsupfilb  44031  faosnf0.11b  44040  ifpidg  44104  ifpid1g  44107  ifpor123g  44121  dfsucon  44136  undmrnresiss  44217  elintima  44266  df3or2  44381  dfhe3  44388  dffrege76  44552  dffrege115  44591  frege131  44607  ntrneikb  44707  ismnuprim  44891  ismnushort  44898  pm14.12  45018  dfvd2an  45178  dfvd3  45187  dfvd3an  45190  uun2221  45408  uun2221p1  45409  uun2221p2  45410  sswfaxreg  45583  modelac8prim  45588  disjinfi  45797  supxrleubrnmptf  46052  fsummulc1f  46174  fsumiunss  46178  fnlimfvre2  46278  limsupreuz  46338  dvmptmulf  46538  dvnmul  46544  dvmptfprodlem  46545  dvnprodlem2  46548  sge0ltfirpmpt2  47027  hoidmv1le  47195  hoidmvle  47201  vonioolem2  47282  smflimlem3  47374  2reu8i  47734  ichexmpl2  48103  setrec2  50353  aacllem  50470