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

Metamath Proof Explorer

Theorem ex3

Description: Apply ex to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018)

		Ref	Expression
	Hypothesis	ex3.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
	Assertion	ex3	$⊢ (φ \land ψ \land χ) \to (θ \to τ)$

Proof

Step	Hyp	Ref	Expression
1		ex3.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
2	1	ex	$⊢ ((φ \land ψ) \land χ) \to (θ \to τ)$
3	2	3impa	$⊢ (φ \land ψ \land χ) \to (θ \to τ)$