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

Metamath Proof Explorer

Theorem alanimi

Description: Variant of al2imi with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011)

		Ref	Expression
	Hypothesis	alanimi.1	$⊢ (φ \land ψ) \to χ$
	Assertion	alanimi	$⊢ (\forall x φ \land \forall x ψ) \to \forall x χ$

Step	Hyp	Ref	Expression
1		alanimi.1	$⊢ (φ \land ψ) \to χ$
2	1	ex	$⊢ φ \to (ψ \to χ)$
3	2	al2imi	$⊢ \forall x φ \to (\forall x ψ \to \forall x χ)$
4	3	imp	$⊢ (\forall x φ \land \forall x ψ) \to \forall x χ$