Theorem imbi1i 351

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ancomst  468  imor  864  3jaob  1444  eximal  1801  nfnbi  1874  19.43  1901  19.37v  2016  19.37  2266  sbor  2339  sb8v  2383  sb8f  2384  dfsb3  2524  mo4f  2593  2mos  2675  neor  3048  r19.43  3129  r19.23v  3188  r3al  3199  r19.23t  3257  sbralieOLD  3341  ceqsralt  3487  ralab  3654  ralrab  3655  euind  3685  reu2  3686  rmo4  3691  rmo3f  3695  rmo4f  3696  reuind  3714  2reu5lem3  3718  rmo3  3840  dfdif3OLD  4070  raldifb  4100  elunant  4134  ralin  4199  inssdif0  4324  ssundif  4438  dfif2  4479  pwss  4576  ralsnsg  4626  ralsng  4631  disjsn  4667  snssb  4738  raldifsni  4752  raldifsnb  4753  unissb  4896  intprg  4936  dfiin2g  4985  iunssf  4997  iunss  4999  disjor  5079  dftr2  5206  axrep1  5225  axrep4v  5229  axrep4  5230  axrep6OLD  5234  axpweq  5304  zfpow  5320  axpow2  5321  reusv2lem4  5355  reusv2  5357  elOLD  5403  dffr6  5599  raliunxp  5807  cotrg  6094  idrefALT  6096  cnvsym  6097  asymref2  6100  dffun4  6529  dffun5  6530  dffun7  6543  fununi  6591  fvn0ssdmfun  7050  dff13  7233  dff14b  7250  fnssintima  7341  zfun  7714  uniex2  7716  dfom2  7843  ralxp3f  8111  frpoins3xpg  8114  frpoins3xp3g  8115  xpord2indlem  8121  xpord3inddlem  8128  soseq  8133  fimaxg  9225  fiint  9265  dfsup2  9384  fiming  9440  oemapso  9631  scottexs  9839  scott0s  9840  iscard2  9928  acnnum  10002  dfac9  10087  dfacacn  10092  kmlem4  10104  kmlem12  10112  axpowndlem3  10551  zfcndun  10567  zfcndpow  10568  zfcndac  10571  axgroth5  10776  axgroth6  10780  addsrmo  11025  mulsrmo  11026  infm3  12145  raluz2  12892  nnwos  12910  ralrp  13009  cotr2g  14983  lo1resb  15582  rlimresb  15583  o1resb  15584  modfsummod  15813  isprm4  16709  acsfn1  17684  acsfn2  17686  lublecllem  18381  isirred2  20457  isdomn5  20747  isdomn2OLD  20749  isdomn3  20752  isdomn4r  20756  iunocv  21721  ist1-2  23395  isnrm2  23406  dfconn2  23467  alexsubALTlem3  24097  ismbl  25576  dyadmbllem  25649  ellimc3  25929  dchrelbas2  27289  dchrelbas3  27290  eqcuts2  27867  addsproplem4  28053  addsproplem6  28055  addsprop  28057  negsproplem4  28112  negsproplem6  28114  negsprop  28116  mulsprop  28211  onsis  28355  ons2ind  28356  isch2  31383  choc0  31486  h1dei  31710  mdsl2i  32482  disjorf  32739  bnj1101  35041  bnj1109  35043  bnj1533  35108  bnj580  35169  bnj864  35178  bnj865  35179  bnj978  35205  bnj1049  35230  bnj1090  35235  bnj1145  35249  fineqvpow  35372  axpowg  35403  vonf1wev  35412  vonf1owevOLD  35414  antnestALT  36005  axextprim  36012  axunprim  36014  axpowprim  36015  untuni  36020  3orit  36027  biimpexp  36028  elintfv  36076  dfon2lem8  36099  dfom5b  36221  iineq1i  36517  ixpeq1i  36521  ss-ax8  36546  mh-regprimbi  36866  mh-infprim2bi  36868  rdgeqoa  37825  wl-equsalcom  38007  wl-sb9v  38013  poimirlem25  38105  poimirlem30  38110  tsim1  38590  inxpss  38777  idinxpss  38778  ref5  38779  idinxpssinxp  38783  ineleq  38814  cocossss  38986  cosscnvssid3  39026  trcoss2  39034  redundpbi1  39175  dfeldisj3  39271  qmapeldisjsim  39320  dfantisymrel5  39325  antisymrelres  39326  cvlsupr3  39929  pmapglbx  40354  isltrn2N  40705  cdlemefrs29bpre0  40981  3factsumint2  42600  3factsumint3  42601  3factsumint4  42602  3factsumint  42603  aks4d1p7  42661  aks4d1p8  42665  fphpd  43354  dford4  43567  fnwe2lem2  43589  unielss  43756  safesnsupfilb  43955  faosnf0.11b  43964  ifpidg  44028  ifpid1g  44031  ifpor123g  44045  dfsucon  44060  undmrnresiss  44141  elintima  44190  df3or2  44305  dfhe3  44312  dffrege76  44476  dffrege115  44515  frege131  44531  ntrneikb  44631  ismnuprim  44831  ismnushort  44838  pm14.12  44958  dfvd2an  45119  dfvd3  45128  dfvd3an  45131  uun2221  45349  uun2221p1  45350  uun2221p2  45351  sswfaxreg  45524  modelac8prim  45529  disjinfi  45731  supxrleubrnmptf  45986  fsummulc1f  46108  fsumiunss  46112  fnlimfvre2  46212  limsupreuz  46272  dvmptmulf  46472  dvnmul  46478  dvmptfprodlem  46479  dvnprodlem2  46482  sge0ltfirpmpt2  46961  hoidmv1le  47129  hoidmvle  47135  vonioolem2  47216  smflimlem3  47308  2reu8i  47668  ichexmpl2  48037  setrec2  50277  aacllem  50383