Metamath Proof Explorer


Theorem ee30

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

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

Proof

Step Hyp Ref Expression
1 ee30.1 φ ψ χ θ
2 ee30.2 τ
3 ee30.3 θ τ η
4 2 a1i χ τ
5 4 a1i ψ χ τ
6 5 a1i φ ψ χ τ
7 1 6 3 ee33 φ ψ χ η