Theorem 3syl 18

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
3syl	⊢ (φ → θ)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 ⊢ (φ → ψ)
2		3syl.2	. . 3 ⊢ (ψ → χ)
3	1, 2	syl 15	. 2 ⊢ (φ → χ)
4		3syl.3	. 2 ⊢ (χ → θ)
5	3, 4	syl 15	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:  nic-ax  1438  merco2  1501  alcomiw  1704  hbn1fw  1705  hba1w  1707  ax5o  1749  hba1OLD  1787  ax16i  2046  hba1-o  2149  ax67to6  2167  ax467  2169  ax467to6  2171  aev-o  2182  ax10-16  2190  mo  2226  eupickb  2269  2eu2  2285  2reu5  3044  sbcco3g  3191  imakexg  4299  intexg  4319  addcexg  4393  nnsucelr  4428  ncfineleq  4477  oddnn  4507  evenodddisj  4516  sfintfin  4532  imaexg  4746  coexg  4749  siexg  4752  fnresdm  5192  foima  5274  f1imacnv  5302  f1osng  5323  oprabid  5550  imageexg  5800  fullfunexg  5859  erth  5968  qsexg  5982  pmex  6005  map0  6025  enpw1  6062  enprmaplem3  6078  enprmaplem6  6081  ncdisjun  6136  ovcelem1  6171  lenc  6223  nchoicelem8  6296  nchoicelem14  6302  nchoicelem17  6305  dmfrec  6316  fnfreclem1  6317  fnfrec  6320