Metamath Proof Explorer


Theorem ee13

Description: e13 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ee13.1 φ ψ
2 ee13.2 φ χ θ τ
3 ee13.3 ψ τ η
4 1 3 syl φ τ η
5 2 4 syl6d φ χ θ η