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

Metamath Proof Explorer

Theorem el2122old

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

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

Proof

Step	Hyp	Ref	Expression
1		el2122old.1	$⊢ ((φ, ψ) \to χ)$
2		el2122old.2	$⊢ (ψ \to θ)$
3		el2122old.3	$⊢ (ψ \to τ)$
4		el2122old.4	$⊢ (χ \land θ \land τ) \to η$
5	1	dfvd2ani	$⊢ (φ \land ψ) \to χ$
6	2	in1	$⊢ ψ \to θ$
7	3	in1	$⊢ ψ \to τ$
8	5 6 7 4	eel2122old	$⊢ (φ \land ψ) \to η$
9	8	dfvd2anir	$⊢ ((φ, ψ) \to η)$