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 ψ φ θ