Metamath Proof Explorer

Theorem e223

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e223.1 ⊢ φ , ψ → χ
e223.2 ⊢ φ , ψ → θ
e223.3 ⊢ φ , ψ , τ → η
e223.4 ⊢ χ → θ → η → ζ
Assertion e223 ⊢ φ , ψ , τ → ζ

Proof

Step Hyp Ref Expression
1 e223.1 ⊢ φ , ψ → χ
2 e223.2 ⊢ φ , ψ → θ
3 e223.3 ⊢ φ , ψ , τ → η
4 e223.4 ⊢ χ → θ → η → ζ
5 1 in2 ⊢ φ → ψ → χ
6 5 in1 ⊢ φ → ψ → χ
7 2 in2 ⊢ φ → ψ → θ
8 7 in1 ⊢ φ → ψ → θ
9 3 in3 ⊢ φ , ψ → τ → η
10 9 in2 ⊢ φ → ψ → τ → η
11 10 in1 ⊢ φ → ψ → τ → η
12 6 8 11 4 ee223 ⊢ φ → ψ → τ → ζ
13 12 dfvd3ir ⊢ φ , ψ , τ → ζ