Metamath Proof Explorer


Theorem ee333

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

Ref Expression
Hypotheses ee333.1 φ ψ χ θ
ee333.2 φ ψ χ τ
ee333.3 φ ψ χ η
ee333.4 θ τ η ζ
Assertion ee333 φ ψ χ ζ

Proof

Step Hyp Ref Expression
1 ee333.1 φ ψ χ θ
2 ee333.2 φ ψ χ τ
3 ee333.3 φ ψ χ η
4 ee333.4 θ τ η ζ
5 1 3imp φ ψ χ θ
6 2 3imp φ ψ χ τ
7 3 3imp φ ψ χ η
8 5 6 7 4 syl3c φ ψ χ ζ
9 8 3exp φ ψ χ ζ