Metamath Proof Explorer


Theorem ee223

Description: e223 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ee223.1 φψχ
2 ee223.2 φψθ
3 ee223.3 φψτη
4 ee223.4 χθηζ
5 1 4 syl6 φψθηζ
6 5 com34 φψηθζ
7 6 com23 φηψθζ
8 7 com12 ηφψθζ
9 3 8 syl8 φψτφψθζ
10 9 com34 φψφτψθζ
11 10 pm2.43a φψτψθζ
12 11 com34 φψψτθζ
13 12 pm2.43d φψτθζ
14 13 com34 φψθτζ
15 2 14 mpdd φψτζ