Metamath Proof Explorer


Theorem ee221

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

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

Proof

Step Hyp Ref Expression
1 ee221.1 φψχ
2 ee221.2 φψθ
3 ee221.3 φτ
4 ee221.4 χθτη
5 3 a1d φψτ
6 1 2 5 4 ee222 φψη