This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem e201

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

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

Proof

Step	Hyp	Ref	Expression
1		e201.1	$⊢ (φ, ψ \to χ)$
2		e201.2	$⊢ θ$
3		e201.3	$⊢ (φ \to τ)$
4		e201.4	$⊢ χ \to (θ \to (τ \to η))$
5	2	vd01	$⊢ (φ \to θ)$
6	1 5 3 4	e211	$⊢ (φ, ψ \to η)$