Metamath Proof Explorer


Theorem syland

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004)

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

Proof

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