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 ⊢ φ → ψ → τ → ζ