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  3097  r19.23v  3156  r3al  3167  r19.23t  3225  sbralieOLD  3319  ceqsralt  3473  ralab  3655  ralrab  3656  euind  3686  reu2  3687  rmo4  3692  rmo3f  3696  rmo4f  3697  reuind  3715  2reu5lem3  3719  rmo3  3843  dfdif3OLD  4071  raldifb  4102  elunant  4137  ralin  4202  inssdif0  4327  ssundif  4441  dfif2  4480  pwss  4576  ralsnsg  4624  ralsng  4629  disjsn  4665  snssb  4736  snssgOLD  4738  raldifsni  4749  raldifsnb  4750  unissb  4893  intprg  4934  dfiin2g  4984  disjor  5077  dftr2  5204  axrep1  5222  axrep4v  5226  axrep4  5227  axrep6OLD  5231  axpweq  5293  zfpow  5308  axpow2  5309  reusv2lem4  5343  reusv2  5345  el  5384  dffr6  5579  raliunxp  5786  cotrg  6064  idrefALT  6066  cnvsym  6067  asymref2  6070  dffun4  6499  dffun5  6500  dffun7  6513  fununi  6561  fvn0ssdmfun  7012  dff13  7195  dff14b  7212  fnssintima  7303  zfun  7676  uniex2  7678  dfom2  7808  ralxp3f  8077  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2indlem  8087  xpord3inddlem  8094  soseq  8099  fimaxg  9192  fiint  9235  fiintOLD  9236  dfsup2  9353  fiming  9409  oemapso  9597  scottexs  9802  scott0s  9803  iscard2  9891  acnnum  9965  dfac9  10050  dfacacn  10055  kmlem4  10067  kmlem12  10075  axpowndlem3  10512  zfcndun  10528  zfcndpow  10529  zfcndac  10532  axgroth5  10737  axgroth6  10741  addsrmo  10986  mulsrmo  10987  infm3  12103  raluz2  12817  nnwos  12835  ralrp  12934  cotr2g  14902  lo1resb  15490  rlimresb  15491  o1resb  15492  modfsummod  15720  isprm4  16614  acsfn1  17586  acsfn2  17588  lublecllem  18283  isirred2  20325  isdomn5  20614  isdomn2OLD  20616  isdomn3  20619  isdomn4r  20623  iunocv  21607  ist1-2  23251  isnrm2  23262  dfconn2  23323  alexsubALTlem3  23953  ismbl  25444  dyadmbllem  25517  ellimc3  25797  dchrelbas2  27165  dchrelbas3  27166  eqscut2  27736  addsproplem4  27903  addsproplem6  27905  addsprop  27907  negsproplem4  27961  negsproplem6  27963  negsprop  27965  mulsprop  28057  onsis  28196  isch2  31186  choc0  31289  h1dei  31513  mdsl2i  32285  disjorf  32542  bnj1101  34770  bnj1109  34772  bnj1533  34838  bnj580  34899  bnj864  34908  bnj865  34909  bnj978  34935  bnj1049  34960  bnj1090  34965  bnj1145  34979  fineqvpow  35090  vonf1owev  35100  antnestALT  35686  axextprim  35693  axunprim  35695  axpowprim  35696  untuni  35701  3orit  35708  biimpexp  35709  elintfv  35757  dfon2lem8  35783  dfom5b  35905  iineq1i  36189  ixpeq1i  36193  ss-ax8  36218  rdgeqoa  37363  wl-equsalcom  37536  wl-sb9v  37542  poimirlem25  37644  poimirlem30  37649  tsim1  38129  inxpss  38304  idinxpss  38305  ref5  38306  idinxpssinxp  38310  ineleq  38341  cocossss  38432  cosscnvssid3  38472  trcoss2  38480  redundpbi1  38627  dfeldisj3  38716  dfantisymrel5  38759  antisymrelres  38760  cvlsupr3  39342  pmapglbx  39768  isltrn2N  40119  cdlemefrs29bpre0  40395  3factsumint2  42015  3factsumint3  42016  3factsumint4  42017  3factsumint  42018  aks4d1p7  42076  aks4d1p8  42080  fphpd  42809  dford4  43022  fnwe2lem2  43044  unielss  43211  safesnsupfilb  43411  faosnf0.11b  43420  ifpidg  43484  ifpid1g  43487  ifpor123g  43501  dfsucon  43516  undmrnresiss  43597  elintima  43646  df3or2  43761  dfhe3  43768  dffrege76  43932  dffrege115  43971  frege131  43987  ntrneikb  44087  ismnuprim  44287  ismnushort  44294  pm14.12  44414  dfvd2an  44576  dfvd3  44585  dfvd3an  44588  uun2221  44806  uun2221p1  44807  uun2221p2  44808  sswfaxreg  44981  modelac8prim  44986  disjinfi  45190  supxrleubrnmptf  45450  fsummulc1f  45572  fsumiunss  45576  fnlimfvre2  45678  limsupreuz  45738  dvmptmulf  45938  dvnmul  45944  dvmptfprodlem  45945  dvnprodlem2  45948  sge0ltfirpmpt2  46427  hoidmv1le  46595  hoidmvle  46601  vonioolem2  46682  smflimlem3  46774  2reu8i  47117  ichexmpl2  47474  setrec2  49700  aacllem  49806