Theorem sylib 188

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylib.1	⊢ (φ → ψ)
sylib.2	⊢ (ψ ↔ χ)

Assertion

Ref	Expression
sylib	⊢ (φ → χ)

Proof of Theorem sylib

Step	Hyp	Ref	Expression
1		sylib.1	. 2 ⊢ (φ → ψ)
2		sylib.2	. . 3 ⊢ (ψ ↔ χ)
3	2	biimpi 186	. 2 ⊢ (ψ → χ)
4	1, 3	syl 15	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ↔ wb 176

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 177

This theorem is referenced by:  bicomd  192  pm5.74d  238  bitri  240  3imtr3i  256  ord  366  orcomd  377  ancomd  438  pm4.71d  615  pm4.71rd  616  pm5.32d  620  imdistand  673  pclem6  896  3mix3  1126  ecase23d  1285  nic-ax  1438  nexdh  1589  exlimivOLD  1698  exlimd  1806  cbv3hv  1850  excomimOLD  1858  sbequi  2059  sbn  2062  spsbe  2075  spsbbi  2077  sb6rf  2091  sb9i  2094  eu2  2229  2euex  2276  2eu1  2284  eqcomd  2358  3eltr3g  2435  abbid  2467  neneqd  2533  syl5eqner  2542  3netr3g  2545  necon1bi  2560  necon4ai  2576  necon4i  2577  necomd  2600  r19.21bi  2713  nrexdv  2718  rexlimd  2736  rabbidva  2851  elisset  2870  euind  3024  rmoan  3035  reuind  3040  spsbc  3059  spesbc  3128  3sstr3g  3312  syl6sseq  3318  un00  3587  disjpss  3602  pssnel  3616  difprsn1  3848  diftpsn3  3850  difsnid  3855  ssunsn2  3866  sneqr  3873  unsneqsn  3888  intab  3957  uniintsn  3964  iinrab2  4030  riinn0  4041  rintn0  4057  preqr1  4125  preq12b  4128  iotanul  4355  iotacl  4363  dfiota4  4373  0nelsuc  4401  nnsucelrlem3  4427  nnsucelrlem4  4428  nndisjeq  4430  prepeano4  4452  ltfinirr  4458  lenltfin  4470  ssfin  4471  vfinnc  4472  ncfinlower  4484  nnpw1ex  4485  tfinltfin  4502  evenodddisj  4517  nnadjoin  4521  tfinnn  4535  sfinltfin  4536  sfin111  4537  vfinncvntsp  4550  vfinspsslem1  4551  vfinspeqtncv  4554  nulnnn  4557  phialllem1  4617  opeqex  4622  3brtr3g  4671  opeliunxp2  4823  rexxpf  4829  brel  4831  dmxp  4924  resopab2  5002  ndmima  5026  dmsnopss  5068  funeu  5132  funeu2  5133  funcnvuni  5162  imadif  5172  fneu2  5189  f00  5250  foconst  5281  foimacnv  5304  resdif  5307  resin  5308  f1ococnv2  5310  fv3  5342  dff3  5421  fsn  5433  fnressn  5439  isores1  5495  swapf1o  5512  resoprab2  5583  funoprabg  5584  fnmpt  5690  fmpt  5693  fmptd  5695  fnmpt2  5733  trtxp  5782  oqelins4  5795  qrpprod  5837  frds  5936  erth  5969  erdisj  5973  elqsn0  5994  mapsn  6027  fundmen  6044  enadjlem1  6060  enadj  6061  enpw1  6063  enprmaplem5  6081  nenpw1pwlem2  6086  mucnc  6132  ncdisjun  6137  peano4nc  6151  ncssfin  6152  ncspw1eu  6160  nntccl  6171  fnce  6177  ce0nnuli  6179  ce0addcnnul  6180  sbthlem1  6204  sbth  6207  dflec3  6222  0lt1c  6259  nmembers1lem2  6270  nncdiv3  6278  spacssnc  6285  nchoicelem12  6301  nchoicelem14  6303  nchoicelem17  6306  frecxp  6315