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	$⊢ (φ, ψ \to χ)$
		e223.2	$⊢ (φ, ψ \to θ)$
		e223.3	$⊢ (φ, ψ, τ \to η)$
		e223.4	$⊢ χ \to (θ \to (η \to ζ))$
	Assertion	e223	$⊢ (φ, ψ, τ \to ζ)$

Proof

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