Metamath Proof Explorer


Theorem syl56

Description: Combine syl5 and syl6 . (Contributed by NM, 14-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 syl56.1 φ ψ
2 syl56.2 χ ψ θ
3 syl56.3 θ τ
4 2 3 syl6 χ ψ τ
5 1 4 syl5 χ φ τ