Theorem syl8 76

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

Ref	Expression
syl8.1	|- ( ph -> ( ps -> ( ch -> th ) ) )
syl8.2	|- ( th -> ta )

Assertion

Ref	Expression
syl8	|- ( ph -> ( ps -> ( ch -> ta ) ) )

Proof of Theorem syl8

Step	Hyp	Ref	Expression
1		syl8.1	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
2		syl8.2	. . 3 |- ( th -> ta )
3	2	a1i 11	. 2 |- ( ph -> ( th -> ta ) )
4	1, 3	syl6d 75	1 |- ( ph -> ( ps -> ( ch -> ta ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  a1ddd  80  com45  97  syl8ib  246  imp5a  624  3exp  1264  3imp3i2an  1278  nfimt  1821  suctrOLD  5809  ssorduni  6985  tfindsg  7060  findsg  7093  tz7.49  7540  nneneq  8143  dfac2  8953  qreccl  11808  dvdsaddre2b  15029  cmpsub  21203  fclsopni  21819  sumdmdlem2  29278  nocvxminlem  31893  idinside  32191  axc11n11r  32673  isbasisrelowllem1  33203  isbasisrelowllem2  33204  prtlem15  34160  prtlem17  34161  ee3bir  38709  ee233  38725  onfrALTlem2  38761  ee223  38859  ee33VD  39115  rngccatidALTV  41989  ringccatidALTV  42052