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 χθη