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  1783  nfnbi  1856  19.43  1883  19.37v  1998  19.37  2239  sbor  2312  sb8v  2357  sb8f  2358  dfsb3  2498  mo4f  2567  2mos  2649  2mosOLD  2650  neor  3024  r19.43  3104  r19.23v  3163  r3al  3174  r19.23t  3232  sbralieOLD  3324  ceqsralt  3475  ralab  3651  ralrab  3652  euind  3682  reu2  3683  rmo4  3688  rmo3f  3692  rmo4f  3693  reuind  3711  2reu5lem3  3715  rmo3  3839  dfdif3OLD  4070  raldifb  4101  elunant  4136  ralin  4201  inssdif0  4326  ssundif  4440  dfif2  4481  pwss  4577  ralsnsg  4627  ralsng  4632  disjsn  4668  snssb  4739  raldifsni  4751  raldifsnb  4752  unissb  4896  intprg  4936  dfiin2g  4986  iunssf  4998  iunss  5000  disjor  5080  dftr2  5207  axrep1  5225  axrep4v  5229  axrep4  5230  axrep6OLD  5234  axpweq  5296  zfpow  5311  axpow2  5312  reusv2lem4  5346  reusv2  5348  el  5387  dffr6  5580  raliunxp  5788  cotrg  6068  idrefALT  6070  cnvsym  6071  asymref2  6074  dffun4  6505  dffun5  6506  dffun7  6519  fununi  6567  fvn0ssdmfun  7019  dff13  7200  dff14b  7217  fnssintima  7308  zfun  7681  uniex2  7683  dfom2  7810  ralxp3f  8079  frpoins3xpg  8082  frpoins3xp3g  8083  xpord2indlem  8089  xpord3inddlem  8096  soseq  8101  fimaxg  9187  fiint  9227  dfsup2  9347  fiming  9403  oemapso  9591  scottexs  9799  scott0s  9800  iscard2  9888  acnnum  9962  dfac9  10047  dfacacn  10052  kmlem4  10064  kmlem12  10072  axpowndlem3  10510  zfcndun  10526  zfcndpow  10527  zfcndac  10530  axgroth5  10735  axgroth6  10739  addsrmo  10984  mulsrmo  10985  infm3  12101  raluz2  12810  nnwos  12828  ralrp  12927  cotr2g  14899  lo1resb  15487  rlimresb  15488  o1resb  15489  modfsummod  15717  isprm4  16611  acsfn1  17584  acsfn2  17586  lublecllem  18281  isirred2  20357  isdomn5  20643  isdomn2OLD  20645  isdomn3  20648  isdomn4r  20652  iunocv  21636  ist1-2  23291  isnrm2  23302  dfconn2  23363  alexsubALTlem3  23993  ismbl  25483  dyadmbllem  25556  ellimc3  25836  dchrelbas2  27204  dchrelbas3  27205  eqcuts2  27782  addsproplem4  27968  addsproplem6  27970  addsprop  27972  negsproplem4  28027  negsproplem6  28029  negsprop  28031  mulsprop  28126  onsis  28270  ons2ind  28271  isch2  31298  choc0  31401  h1dei  31625  mdsl2i  32397  disjorf  32654  bnj1101  34940  bnj1109  34942  bnj1533  35008  bnj580  35069  bnj864  35078  bnj865  35079  bnj978  35105  bnj1049  35130  bnj1090  35135  bnj1145  35149  fineqvpow  35271  vonf1owev  35302  antnestALT  35888  axextprim  35895  axunprim  35897  axpowprim  35898  untuni  35903  3orit  35910  biimpexp  35911  elintfv  35959  dfon2lem8  35982  dfom5b  36104  iineq1i  36390  ixpeq1i  36394  ss-ax8  36419  bj-df-sb  36853  rdgeqoa  37575  wl-equsalcom  37748  wl-sb9v  37754  poimirlem25  37846  poimirlem30  37851  tsim1  38331  inxpss  38510  idinxpss  38511  ref5  38512  idinxpssinxp  38516  ineleq  38547  cocossss  38699  cosscnvssid3  38739  trcoss2  38747  redundpbi1  38888  dfeldisj3  38978  dfantisymrel5  39021  antisymrelres  39022  cvlsupr3  39604  pmapglbx  40029  isltrn2N  40380  cdlemefrs29bpre0  40656  3factsumint2  42276  3factsumint3  42277  3factsumint4  42278  3factsumint  42279  aks4d1p7  42337  aks4d1p8  42341  fphpd  43058  dford4  43271  fnwe2lem2  43293  unielss  43460  safesnsupfilb  43659  faosnf0.11b  43668  ifpidg  43732  ifpid1g  43735  ifpor123g  43749  dfsucon  43764  undmrnresiss  43845  elintima  43894  df3or2  44009  dfhe3  44016  dffrege76  44180  dffrege115  44219  frege131  44235  ntrneikb  44335  ismnuprim  44535  ismnushort  44542  pm14.12  44662  dfvd2an  44823  dfvd3  44832  dfvd3an  44835  uun2221  45053  uun2221p1  45054  uun2221p2  45055  sswfaxreg  45228  modelac8prim  45233  disjinfi  45436  supxrleubrnmptf  45695  fsummulc1f  45817  fsumiunss  45821  fnlimfvre2  45921  limsupreuz  45981  dvmptmulf  46181  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem2  46191  sge0ltfirpmpt2  46670  hoidmv1le  46838  hoidmvle  46844  vonioolem2  46925  smflimlem3  47017  2reu8i  47359  ichexmpl2  47716  setrec2  49940  aacllem  50046