Metamath Proof Explorer

Theorem e333

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

		Ref	Expression
	Hypotheses	e333.1	$⊢ (φ, ψ, χ \to θ)$
		e333.2	$⊢ (φ, ψ, χ \to τ)$
		e333.3	$⊢ (φ, ψ, χ \to η)$
		e333.4	$⊢ θ \to (τ \to (η \to ζ))$
	Assertion	e333	$⊢ (φ, ψ, χ \to ζ)$

Proof

Step	Hyp	Ref	Expression
1		e333.1	$⊢ (φ, ψ, χ \to θ)$
2		e333.2	$⊢ (φ, ψ, χ \to τ)$
3		e333.3	$⊢ (φ, ψ, χ \to η)$
4		e333.4	$⊢ θ \to (τ \to (η \to ζ))$
5	3	dfvd3i	$⊢ φ \to (ψ \to (χ \to η))$
6	5	3imp	$⊢ (φ \land ψ \land χ) \to η$
7	1	dfvd3i	$⊢ φ \to (ψ \to (χ \to θ))$
8	7	3imp	$⊢ (φ \land ψ \land χ) \to θ$
9	2	dfvd3i	$⊢ φ \to (ψ \to (χ \to τ))$
10	9	3imp	$⊢ (φ \land ψ \land χ) \to τ$
11	8 10 4	syl2im	$⊢ (φ \land ψ \land χ) \to ((φ \land ψ \land χ) \to (η \to ζ))$
12	11	pm2.43i	$⊢ (φ \land ψ \land χ) \to (η \to ζ)$
13	6 12	syl5com	$⊢ (φ \land ψ \land χ) \to ((φ \land ψ \land χ) \to ζ)$
14	13	pm2.43i	$⊢ (φ \land ψ \land χ) \to ζ$
15	14	3exp	$⊢ φ \to (ψ \to (χ \to ζ))$
16	15	dfvd3ir	$⊢ (φ, ψ, χ \to ζ)$