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  2492  mo4f  2560  2mos  2642  2mosOLD  2643  neor  3017  r19.43  3101  r19.23v  3160  r3al  3173  r19.23t  3231  sbralieOLD  3325  ceqsralt  3479  ralab  3661  ralrab  3662  euind  3692  reu2  3693  rmo4  3698  rmo3f  3702  rmo4f  3703  reuind  3721  2reu5lem3  3725  rmo3  3849  dfdif3OLD  4077  raldifb  4108  elunant  4143  ralin  4208  inssdif0  4333  ssundif  4447  dfif2  4486  pwss  4582  ralsnsg  4630  ralsng  4635  disjsn  4671  snssb  4742  snssgOLD  4744  raldifsni  4755  raldifsnb  4756  unissb  4899  unissbOLD  4900  intprg  4941  dfiin2g  4991  disjor  5084  dftr2  5211  axrep1  5230  axrep4v  5234  axrep4  5235  axrep6OLD  5239  axpweq  5301  zfpow  5316  axpow2  5317  reusv2lem4  5351  reusv2  5353  el  5392  dffr6  5587  raliunxp  5793  cotrg  6069  cotrgOLD  6070  idrefALT  6072  cnvsym  6073  cnvsymOLD  6074  asymref2  6078  dffun4  6513  dffun5  6514  dffun7  6527  fununi  6575  fvn0ssdmfun  7028  dff13  7211  dff14b  7228  fnssintima  7319  zfun  7692  uniex2  7694  dfom2  7824  ralxp3f  8093  frpoins3xpg  8096  frpoins3xp3g  8097  xpord2indlem  8103  xpord3inddlem  8110  soseq  8115  fimaxg  9210  fiint  9253  fiintOLD  9254  dfsup2  9371  fiming  9427  oemapso  9611  scottexs  9816  scott0s  9817  iscard2  9905  acnnum  9981  dfac9  10066  dfacacn  10071  kmlem4  10083  kmlem12  10091  axpowndlem3  10528  zfcndun  10544  zfcndpow  10545  zfcndac  10548  axgroth5  10753  axgroth6  10757  addsrmo  11002  mulsrmo  11003  infm3  12118  raluz2  12832  nnwos  12850  ralrp  12949  cotr2g  14918  lo1resb  15506  rlimresb  15507  o1resb  15508  modfsummod  15736  isprm4  16630  acsfn1  17598  acsfn2  17600  lublecllem  18295  isirred2  20306  isdomn5  20595  isdomn2OLD  20597  isdomn3  20600  isdomn4r  20604  iunocv  21566  ist1-2  23210  isnrm2  23221  dfconn2  23282  alexsubALTlem3  23912  ismbl  25403  dyadmbllem  25476  ellimc3  25756  dchrelbas2  27124  dchrelbas3  27125  eqscut2  27694  addsproplem4  27855  addsproplem6  27857  addsprop  27859  negsproplem4  27913  negsproplem6  27915  negsprop  27917  mulsprop  28009  onsis  28148  isch2  31125  choc0  31228  h1dei  31452  mdsl2i  32224  disjorf  32481  bnj1101  34747  bnj1109  34749  bnj1533  34815  bnj580  34876  bnj864  34885  bnj865  34886  bnj978  34912  bnj1049  34937  bnj1090  34942  bnj1145  34956  fineqvpow  35059  vonf1owev  35068  antnestALT  35654  axextprim  35661  axunprim  35663  axpowprim  35664  untuni  35669  3orit  35676  biimpexp  35677  elintfv  35725  dfon2lem8  35751  dfom5b  35873  iineq1i  36157  ixpeq1i  36161  ss-ax8  36186  rdgeqoa  37331  wl-equsalcom  37504  wl-sb9v  37510  poimirlem25  37612  poimirlem30  37617  tsim1  38097  inxpss  38272  idinxpss  38273  ref5  38274  idinxpssinxp  38278  ineleq  38309  cocossss  38400  cosscnvssid3  38440  trcoss2  38448  redundpbi1  38595  dfeldisj3  38684  dfantisymrel5  38727  antisymrelres  38728  cvlsupr3  39310  pmapglbx  39736  isltrn2N  40087  cdlemefrs29bpre0  40363  3factsumint2  41983  3factsumint3  41984  3factsumint4  41985  3factsumint  41986  aks4d1p7  42044  aks4d1p8  42048  fphpd  42777  dford4  42991  fnwe2lem2  43013  unielss  43180  safesnsupfilb  43380  faosnf0.11b  43389  ifpidg  43453  ifpid1g  43456  ifpor123g  43470  dfsucon  43485  undmrnresiss  43566  elintima  43615  df3or2  43730  dfhe3  43737  dffrege76  43901  dffrege115  43940  frege131  43956  ntrneikb  44056  ismnuprim  44256  ismnushort  44263  pm14.12  44383  dfvd2an  44545  dfvd3  44554  dfvd3an  44557  uun2221  44775  uun2221p1  44776  uun2221p2  44777  sswfaxreg  44950  modelac8prim  44955  disjinfi  45159  supxrleubrnmptf  45420  fsummulc1f  45542  fsumiunss  45546  fnlimfvre2  45648  limsupreuz  45708  dvmptmulf  45908  dvnmul  45914  dvmptfprodlem  45915  dvnprodlem2  45918  sge0ltfirpmpt2  46397  hoidmv1le  46565  hoidmvle  46571  vonioolem2  46652  smflimlem3  46744  2reu8i  47087  ichexmpl2  47444  setrec2  49657  aacllem  49763