Metamath Proof Explorer


Theorem syl9

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993) (Proof shortened by Josh Purinton, 29-Dec-2000)

Ref Expression
Hypotheses syl9.1 φψχ
syl9.2 θχτ
Assertion syl9 φθψτ

Proof

Step Hyp Ref Expression
1 syl9.1 φψχ
2 syl9.2 θχτ
3 2 a1i φθχτ
4 1 3 syl5d φθψτ