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

Metamath Proof Explorer

Theorem el123

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

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

Proof

Step	Hyp	Ref	Expression
1		el123.1	$⊢ (φ \to ψ)$
2		el123.2	$⊢ (χ \to θ)$
3		el123.3	$⊢ (τ \to η)$
4		el123.4	$⊢ (ψ \land θ \land η) \to ζ$
5	1	in1	$⊢ φ \to ψ$
6	2	in1	$⊢ χ \to θ$
7	3	in1	$⊢ τ \to η$
8	5 6 7 4	syl3an	$⊢ (φ \land χ \land τ) \to ζ$
9	8	dfvd3anir	$⊢ ((φ, χ, τ) \to ζ)$