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  466  imor  860  3jaob  1435  eximal  1790  nfnbi  1863  19.43  1890  19.37v  2005  19.37  2246  sbor  2319  sb8v  2363  sb8f  2364  dfsb3  2504  mo4f  2573  2mos  2655  neor  3028  r19.43  3109  r19.23v  3168  r3al  3179  r19.23t  3237  sbralieOLD  3321  ceqsralt  3467  ralab  3635  ralrab  3636  euind  3666  reu2  3667  rmo4  3672  rmo3f  3676  rmo4f  3677  reuind  3695  2reu5lem3  3699  rmo3  3822  dfdif3OLD  4051  raldifb  4081  elunant  4115  ralin  4179  inssdif0  4304  ssundif  4417  dfif2  4458  pwss  4554  ralsnsg  4604  ralsng  4609  disjsn  4645  snssb  4716  raldifsni  4730  raldifsnb  4731  unissb  4873  intprg  4913  dfiin2g  4962  iunssf  4974  iunss  4976  disjor  5056  dftr2  5183  axrep1  5202  axrep4v  5206  axrep4  5207  axrep6OLD  5211  axpweq  5281  zfpow  5297  axpow2  5298  reusv2lem4  5332  reusv2  5334  elOLD  5380  dffr6  5576  raliunxp  5783  cotrg  6067  idrefALT  6069  cnvsym  6070  asymref2  6073  dffun4  6501  dffun5  6502  dffun7  6515  fununi  6563  fvn0ssdmfun  7018  dff13  7201  dff14b  7218  fnssintima  7309  zfun  7682  uniex2  7684  dfom2  7811  ralxp3f  8079  frpoins3xpg  8082  frpoins3xp3g  8083  xpord2indlem  8089  xpord3inddlem  8096  soseq  8101  fimaxg  9191  fiint  9231  dfsup2  9351  fiming  9407  oemapso  9598  scottexs  9806  scott0s  9807  iscard2  9895  acnnum  9969  dfac9  10054  dfacacn  10059  kmlem4  10071  kmlem12  10079  axpowndlem3  10518  zfcndun  10534  zfcndpow  10535  zfcndac  10538  axgroth5  10743  axgroth6  10747  addsrmo  10992  mulsrmo  10993  infm3  12110  raluz2  12842  nnwos  12860  ralrp  12959  cotr2g  14933  lo1resb  15521  rlimresb  15522  o1resb  15523  modfsummod  15752  isprm4  16648  acsfn1  17622  acsfn2  17624  lublecllem  18319  isirred2  20395  isdomn5  20685  isdomn2OLD  20687  isdomn3  20690  isdomn4r  20694  iunocv  21659  ist1-2  23333  isnrm2  23344  dfconn2  23405  alexsubALTlem3  24035  ismbl  25514  dyadmbllem  25587  ellimc3  25867  dchrelbas2  27221  dchrelbas3  27222  eqcuts2  27798  addsproplem4  27984  addsproplem6  27986  addsprop  27988  negsproplem4  28043  negsproplem6  28045  negsprop  28047  mulsprop  28142  onsis  28286  ons2ind  28287  isch2  31314  choc0  31417  h1dei  31641  mdsl2i  32413  disjorf  32670  bnj1101  34980  bnj1109  34982  bnj1533  35047  bnj580  35108  bnj864  35117  bnj865  35118  bnj978  35144  bnj1049  35169  bnj1090  35174  bnj1145  35188  fineqvpow  35309  axpowg  35340  vonf1owev  35349  antnestALT  35935  axextprim  35942  axunprim  35944  axpowprim  35945  untuni  35950  3orit  35957  biimpexp  35958  elintfv  36006  dfon2lem8  36029  dfom5b  36151  iineq1i  36437  ixpeq1i  36441  ss-ax8  36466  mh-regprimbi  36786  mh-infprim2bi  36788  rdgeqoa  37745  wl-equsalcom  37927  wl-sb9v  37933  poimirlem25  38025  poimirlem30  38030  tsim1  38510  inxpss  38697  idinxpss  38698  ref5  38699  idinxpssinxp  38703  ineleq  38734  cocossss  38906  cosscnvssid3  38946  trcoss2  38954  redundpbi1  39095  dfeldisj3  39191  qmapeldisjsim  39240  dfantisymrel5  39245  antisymrelres  39246  cvlsupr3  39849  pmapglbx  40274  isltrn2N  40625  cdlemefrs29bpre0  40901  3factsumint2  42520  3factsumint3  42521  3factsumint4  42522  3factsumint  42523  aks4d1p7  42581  aks4d1p8  42585  fphpd  43274  dford4  43487  fnwe2lem2  43509  unielss  43676  safesnsupfilb  43875  faosnf0.11b  43884  ifpidg  43948  ifpid1g  43951  ifpor123g  43965  dfsucon  43980  undmrnresiss  44061  elintima  44110  df3or2  44225  dfhe3  44232  dffrege76  44396  dffrege115  44435  frege131  44451  ntrneikb  44551  ismnuprim  44751  ismnushort  44758  pm14.12  44878  dfvd2an  45039  dfvd3  45048  dfvd3an  45051  uun2221  45269  uun2221p1  45270  uun2221p2  45271  sswfaxreg  45444  modelac8prim  45449  disjinfi  45651  supxrleubrnmptf  45906  fsummulc1f  46028  fsumiunss  46032  fnlimfvre2  46132  limsupreuz  46192  dvmptmulf  46392  dvnmul  46398  dvmptfprodlem  46399  dvnprodlem2  46402  sge0ltfirpmpt2  46881  hoidmv1le  47049  hoidmvle  47055  vonioolem2  47136  smflimlem3  47228  2reu8i  47588  ichexmpl2  47957  setrec2  50197  aacllem  50303