Metamath Proof Explorer


Theorem syl9r

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993)

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

Proof

Step Hyp Ref Expression
1 syl9r.1 φ ψ χ
2 syl9r.2 θ χ τ
3 1 2 syl9 φ θ ψ τ
4 3 com12 θ φ ψ τ