This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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