Theorem syl6d 56

Description: A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6d

Step	Hyp	Ref	Expression
1		syl6d.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		syl6d.2	. . 3 |- (ph -> (th -> ta))
3	2	a1d 12	. 2 |- (ph -> (ps -> (th -> ta)))
4	1, 3	syldd 50	1 |- (ph -> (ps -> (ch -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  cbv1 1162  sbi1 1232  omlimcl 4209  ltexprlem7 5148  infmsup 6068  fsum0diaglem2 7257  cncnplem2 7775  nmcopexlem6 9956  nmcfnexlem6 9985

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

Copyright terms: Public domain