Metamath Proof Explorer


Theorem syld3an3

Description: A syllogism inference. (Contributed by NM, 20-May-2007)

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

Proof

Step Hyp Ref Expression
1 syld3an3.1 φ ψ χ θ
2 syld3an3.2 φ ψ θ τ
3 simp1 φ ψ χ φ
4 simp2 φ ψ χ ψ
5 3 4 1 2 syl3anc φ ψ χ τ