Theorem 3syl 18

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

Hypotheses

Ref	Expression
3syl.1	|- (ph -> ps)
3syl.2	|- (ps -> ch)
3syl.3	|- (ch -> th)

Assertion

Ref	Expression
3syl	|- (ph -> th)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- (ph -> ps)
2		3syl.2	. . 3 |- (ps -> ch)
3	1, 2	syl 15	. 2 |- (ph -> ch)
4		3syl.3	. 2 |- (ch -> th)
5	3, 4	syl 15	1 |- (ph -> th)

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  3045  sbcco3g  3192  imakexg  4300  intexg  4320  addcexg  4394  nnsucelr  4429  ncfineleq  4478  oddnn  4508  evenodddisj  4517  sfintfin  4533  imaexg  4747  coexg  4750  siexg  4753  fnresdm  5193  foima  5275  f1imacnv  5303  f1osng  5324  oprabid  5551  imageexg  5801  fullfunexg  5860  erth  5969  qsexg  5983  pmex  6006  map0  6026  enpw1  6063  enprmaplem3  6079  enprmaplem6  6082  ncdisjun  6137  ovcelem1  6172  lenc  6224  nchoicelem8  6297  nchoicelem14  6303  nchoicelem17  6306  dmfrec  6317  fnfreclem1  6318  fnfrec  6321