Metamath Proof Explorer


Theorem ee13an

Description: e13an without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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