Metamath Proof Explorer


Theorem syldc

Description: Syllogism deduction. Commuted form of syld . (Contributed by BJ, 25-Oct-2021)

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

Proof

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