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  3326  ceqsralt  3477  ralab  3653  ralrab  3654  euind  3684  reu2  3685  rmo4  3690  rmo3f  3694  rmo4f  3695  reuind  3713  2reu5lem3  3717  rmo3  3841  dfdif3OLD  4072  raldifb  4103  elunant  4138  ralin  4203  inssdif0  4328  ssundif  4442  dfif2  4483  pwss  4579  ralsnsg  4629  ralsng  4634  disjsn  4670  snssb  4741  raldifsni  4753  raldifsnb  4754  unissb  4898  intprg  4938  dfiin2g  4988  iunssf  5000  iunss  5002  disjor  5082  dftr2  5209  axrep1  5227  axrep4v  5231  axrep4  5232  axrep6OLD  5236  axpweq  5298  zfpow  5313  axpow2  5314  reusv2lem4  5348  reusv2  5350  el  5394  dffr6  5588  raliunxp  5796  cotrg  6076  idrefALT  6078  cnvsym  6079  asymref2  6082  dffun4  6513  dffun5  6514  dffun7  6527  fununi  6575  fvn0ssdmfun  7028  dff13  7210  dff14b  7227  fnssintima  7318  zfun  7691  uniex2  7693  dfom2  7820  ralxp3f  8089  frpoins3xpg  8092  frpoins3xp3g  8093  xpord2indlem  8099  xpord3inddlem  8106  soseq  8111  fimaxg  9199  fiint  9239  dfsup2  9359  fiming  9415  oemapso  9603  scottexs  9811  scott0s  9812  iscard2  9900  acnnum  9974  dfac9  10059  dfacacn  10064  kmlem4  10076  kmlem12  10084  axpowndlem3  10522  zfcndun  10538  zfcndpow  10539  zfcndac  10542  axgroth5  10747  axgroth6  10751  addsrmo  10996  mulsrmo  10997  infm3  12113  raluz2  12822  nnwos  12840  ralrp  12939  cotr2g  14911  lo1resb  15499  rlimresb  15500  o1resb  15501  modfsummod  15729  isprm4  16623  acsfn1  17596  acsfn2  17598  lublecllem  18293  isirred2  20369  isdomn5  20655  isdomn2OLD  20657  isdomn3  20660  isdomn4r  20664  iunocv  21648  ist1-2  23303  isnrm2  23314  dfconn2  23375  alexsubALTlem3  24005  ismbl  25495  dyadmbllem  25568  ellimc3  25848  dchrelbas2  27216  dchrelbas3  27217  eqcuts2  27794  addsproplem4  27980  addsproplem6  27982  addsprop  27984  negsproplem4  28039  negsproplem6  28041  negsprop  28043  mulsprop  28138  onsis  28282  ons2ind  28283  isch2  31311  choc0  31414  h1dei  31638  mdsl2i  32410  disjorf  32666  bnj1101  34961  bnj1109  34963  bnj1533  35028  bnj580  35089  bnj864  35098  bnj865  35099  bnj978  35125  bnj1049  35150  bnj1090  35155  bnj1145  35169  fineqvpow  35293  vonf1owev  35324  antnestALT  35910  axextprim  35917  axunprim  35919  axpowprim  35920  untuni  35925  3orit  35932  biimpexp  35933  elintfv  35981  dfon2lem8  36004  dfom5b  36126  iineq1i  36412  ixpeq1i  36416  ss-ax8  36441  bj-df-sb  36897  rdgeqoa  37625  wl-equsalcom  37798  wl-sb9v  37804  poimirlem25  37896  poimirlem30  37901  tsim1  38381  inxpss  38568  idinxpss  38569  ref5  38570  idinxpssinxp  38574  ineleq  38605  cocossss  38777  cosscnvssid3  38817  trcoss2  38825  redundpbi1  38966  dfeldisj3  39062  qmapeldisjsim  39111  dfantisymrel5  39116  antisymrelres  39117  cvlsupr3  39720  pmapglbx  40145  isltrn2N  40496  cdlemefrs29bpre0  40772  3factsumint2  42392  3factsumint3  42393  3factsumint4  42394  3factsumint  42395  aks4d1p7  42453  aks4d1p8  42457  fphpd  43173  dford4  43386  fnwe2lem2  43408  unielss  43575  safesnsupfilb  43774  faosnf0.11b  43783  ifpidg  43847  ifpid1g  43850  ifpor123g  43864  dfsucon  43879  undmrnresiss  43960  elintima  44009  df3or2  44124  dfhe3  44131  dffrege76  44295  dffrege115  44334  frege131  44350  ntrneikb  44450  ismnuprim  44650  ismnushort  44657  pm14.12  44777  dfvd2an  44938  dfvd3  44947  dfvd3an  44950  uun2221  45168  uun2221p1  45169  uun2221p2  45170  sswfaxreg  45343  modelac8prim  45348  disjinfi  45551  supxrleubrnmptf  45809  fsummulc1f  45931  fsumiunss  45935  fnlimfvre2  46035  limsupreuz  46095  dvmptmulf  46295  dvnmul  46301  dvmptfprodlem  46302  dvnprodlem2  46305  sge0ltfirpmpt2  46784  hoidmv1le  46952  hoidmvle  46958  vonioolem2  47039  smflimlem3  47131  2reu8i  47473  ichexmpl2  47830  setrec2  50054  aacllem  50160