Metamath Proof Explorer


Theorem ee002

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

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

Proof

Step Hyp Ref Expression
1 ee002.1 φ
2 ee002.2 ψ
3 ee002.3 χ θ τ
4 ee002.4 φ ψ τ η
5 1 a1i θ φ
6 5 a1i χ θ φ
7 2 a1i θ ψ
8 7 a1i χ θ ψ
9 6 8 3 4 ee222 χ θ η