Metamath Proof Explorer


Theorem 3syld

Description: Triple syllogism deduction. Deduction associated with 3syld . (Contributed by Jeff Hankins, 4-Aug-2009)

Ref Expression
Hypotheses 3syld.1 φψχ
3syld.2 φχθ
3syld.3 φθτ
Assertion 3syld φψτ

Proof

Step Hyp Ref Expression
1 3syld.1 φψχ
2 3syld.2 φχθ
3 3syld.3 φθτ
4 1 2 syld φψθ
5 4 3 syld φψτ