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 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ancomst  470  imor  867  3jaob  1453  eximal  1814  nfnbi  1887  19.43  1914  19.37v  2029  19.37  2268  sbor  2339  sb8v  2382  sb8f  2383  dfsb3  2523  mo4f  2592  2mos  2674  neor  3047  r19.43  3130  r19.23v  3189  r3al  3200  r19.23t  3258  sbralieOLD  3340  ceqsralt  3484  ralab  3650  ralrab  3651  euind  3681  reu2  3682  rmo4  3687  rmo3f  3691  rmo4f  3692  reuind  3710  2reu5lem3  3714  rmo3  3836  raldifb  4084  ralin  4145  elunant  4181  inssdif0OLD  4322  ssundif  4442  dfif2  4483  pwss  4581  ralsnsg  4627  ralsng  4632  disjsn  4668  snssb  4739  raldifsni  4754  raldifsnb  4755  unissb  4900  intprg  4940  dfiin2g  4988  iunssf  5000  iunss  5002  disjor  5084  dftr2  5213  axrep1  5232  axrep4v  5236  axrep4  5237  axpweq  5311  zfpow  5327  axpow2  5328  reusv2lem4  5362  reusv2  5364  el.OLD  5406  dffr6  5606  raliunxp  5816  cotrg  6106  idrefALT  6108  cnvsym  6109  asymref2  6112  dffun4  6554  dffun5  6555  dffun7  6570  fununi  6618  fvn0ssdmfun  7077  dff13  7260  dff14b  7277  fnssintima  7374  zfun  7754  uniex2OLD  7757  dfom2  7881  ovmptss  8106  fnwe2lem3  8151  ralxp3f  8158  frpoins3xpg  8161  frpoins3xp3g  8162  xpord2indlem  8168  xpord3inddlem  8175  soseq  8180  fimaxg  9283  fiint  9323  dfsup2  9441  fiming  9497  oemapso  9688  scottexsOLD  9948  scott0bsOLD  9950  setrec2  9982  iscard2  10062  acnnum  10136  dfac9  10220  dfacacn  10225  kmlem4  10237  kmlem12  10245  axpowndlem3  10689  zfcndun  10705  zfcndpow  10706  zfcndac  10709  axgroth5  10914  axgroth6  10918  addsrmo  11163  mulsrmo  11164  infm3  12281  raluz2  13029  nnwos  13047  ralrp  13147  cotr2g  15136  lo1resb  15738  rlimresb  15739  o1resb  15740  modfsummod  15968  isprm4  16866  acsfn1  17842  acsfn2  17844  lublecllem  18539  isirred2  20658  isdomn5  20969  isdomn3  20973  isdomn4r  20977  iunocv  21994  ist1-2  23672  isnrm2  23683  dfconn2  23744  alexsubALTlem3  24375  ismbl  25854  dyadmbllem  25927  ellimc3  26206  dchrelbas2  27571  dchrelbas3  27572  eqcuts2  28179  addsproplem4  28365  addsproplem6  28367  addsprop  28369  negsproplem4  28424  negsproplem6  28426  negsprop  28428  mulsprop  28523  onsis  28667  ons2ind  28668  isch2  31832  choc0  31935  h1dei  32159  mdsl2i  32931  disjorf  33222  bnj1101  35463  bnj1109  35465  bnj1533  35530  bnj580  35591  bnj864  35600  bnj865  35601  bnj978  35627  bnj1049  35652  bnj1090  35657  bnj1145  35671  rmo6  35758  fineqvpow  35841  axpowg  35872  vonf1wev  35957  vonf1owevOLD  35959  antnestALT  36547  axextprim  36560  axunprim  36562  axpowprim  36563  untuni  36568  3orit  36575  biimpexp  36576  elintfv  36624  dfon2lem8  36646  dfom5b  36768  iineq1i  37079  ixpeq1i  37083  ss-ax8  37108  mh-regprimbi  37427  mh-infprim2bi  37429  rdgeqoa  38400  wl-equsalcom  38582  wl-sb9v  38588  poimirlem25  38670  poimirlem30  38675  tsim1  39169  inxpss  39356  idinxpss  39357  ref5  39358  idinxpssinxp  39362  ineleq  39393  cocossss  39565  cosscnvssid3  39605  trcoss2  39613  redundpbi1  39754  dfeldisj3  39850  qmapeldisjsim  39899  dfantisymrel5  39904  antisymrelres  39905  cvlsupr3  40508  pmapglbx  40933  isltrn2N  41284  cdlemefrs29bpre0  41560  3factsumint2  43179  3factsumint3  43180  3factsumint4  43181  3factsumint  43182  aks4d1p7  43240  aks4d1p8  43244  fphpd  43930  dford4  44143  unielss  44327  safesnsupfilb  44526  faosnf0.11b  44535  ifpidg  44599  ifpid1g  44602  ifpor123g  44616  dfsucon  44631  undmrnresiss  44711  elintima  44760  df3or2  44875  dfhe3  44882  dffrege76  45046  dffrege115  45085  frege131  45101  ntrneikb  45201  ismnuprim  45385  ismnushort  45392  pm14.12  45512  dfvd2an  45672  dfvd3  45681  dfvd3an  45684  uun2221  45902  uun2221p1  45903  uun2221p2  45904  sswfaxreg  46084  modelac8prim  46089  disjinfi  46314  supxrleubrnmptf  46568  fsummulc1f  46690  fsumiunss  46694  fnlimfvre2  46794  limsupreuz  46854  dvmptmulf  47054  dvnmul  47060  dvmptfprodlem  47061  dvnprodlem2  47064  sge0ltfirpmpt2  47543  hoidmv1le  47711  hoidmvle  47717  vonioolem2  47798  smflimlem3  47890  2reu8i  48290  ichexmpl2  48659  aacllem  51121