Theorem syl5 28

Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	⊢ (φ → ψ)
syl5.2	⊢ (χ → (ψ → θ))

Assertion

Ref	Expression
syl5	⊢ (χ → (φ → θ))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (φ → ψ)
2		syl5.2	. . 3 ⊢ (χ → (ψ → θ))
3	1, 2	syl5com 26	. 2 ⊢ (φ → (χ → θ))
4	3	com12 27	1 ⊢ (χ → (φ → θ))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl56  30  syl2im  34  imim12i  53  pm2.86d  93  con2d  107  con3d  125  nsyli  133  syl5bi  208  syl5bir  209  syl5ib  210  adantld  453  adantrd  454  mpan9  455  pm4.79  566  pm2.36  816  pm4.72  846  ecased  910  ecase3ad  911  syl3an2  1216  alrimdh  1587  ax11w  1721  ax12dgen2  1726  ax5o  1749  spsd  1755  hbnt  1775  nfndOLD  1792  stdpc5OLD  1799  19.21hOLD  1840  cbv3hvOLD  1851  ax12olem5  1931  a16g  1945  hbae  1953  dvelimh  1964  exdistrf  1971  ax11a2  1993  sbft  2025  sbied  2036  sb4  2053  ax11v  2096  ax11vALT  2097  ax5  2146  hbae-o  2153  dvelimf-o  2180  ax11indn  2195  ax11inda2  2199  ax11a2-o  2202  euimmo  2253  mopick  2266  spcimgft  2931  rr19.28v  2982  moeq3  3014  mob2  3017  euind  3024  reuind  3040  sbeqalb  3099  sbcimdv  3108  csbexg  3147  opkthg  4132  nndisjeq  4430  sfin112  4530  sfintfin  4533  sfinltfin  4536  vfinspsslem1  4551  vfinspss  4552  phi11lem1  4596  copsexg  4608  dmcosseq  4974  ssreseq  4998  dfco2a  5082  imadif  5172  dff4  5422  foco2  5427  funfvima2  5461  oprabid  5551  ovmpt4g  5711  ov2gf  5712  fvmptf  5723  fvmptnf  5724  clos1conn  5880  connexd  5932  ectocld  5992  enmap2lem3  6066  enmap1lem3  6072  enprmaplem3  6079  enprmaplem5  6081  enprmaplem6  6082  ncdisjun  6137  nceleq  6150  peano4nc  6151  ncssfin  6152  fce  6189  lectr  6212  leltctr  6213  taddc  6230  tlecg  6231  nclenn  6250  addcdi  6251  ncslesuc  6268  nchoicelem9  6298  nchoicelem15  6304  nchoicelem17  6306  dmfrec  6317  fnfreclem3  6320  fnfrec  6321