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 ( 𝜓 → ( 𝜑𝜃 ) )