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 
|- ( ph -> ( ps -> ch ) )
syld.2 
|- ( ph -> ( ch -> th ) )
Assertion syldc 
|- ( ps -> ( ph -> th ) )

Proof

Step Hyp Ref Expression
1 syld.1 
 |-  ( ph -> ( ps -> ch ) )
2 syld.2 
 |-  ( ph -> ( ch -> th ) )
3 1 2 syld 
 |-  ( ph -> ( ps -> th ) )
4 3 com12 
 |-  ( ps -> ( ph -> th ) )