Theorem syl8 24

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.

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	imim2i 17	. 2 |- ((ch -> th) -> (ch -> ta))
4	1, 3	syl6 22	1 |- (ph -> (ps -> (ch -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl8ib 217  a12studyALT 1378  onfr 2982  ssorduni 2989  findsg 3153  tfindsg 3158  tz7.49 3954  nneneq 4501  aceq6b 4725  ltbtwnpq 5067  reclem3pr 5141  suppsr2 5206  qrecclt 6223  iserzgt0 7163  nmoubi 8395  nmopubt 9789  nmfnleubt 9806  sumdmdlem2 10302

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

Copyright terms: Public domain