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

Metamath Proof Explorer

Theorem 2ax5

Description: Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011)

		Ref	Expression
	Assertion	2ax5	$⊢ φ \to \forall x \forall y φ$

Step	Hyp	Ref	Expression
1		id	$⊢ φ \to φ$
2	1	alrimivv	$⊢ φ \to \forall x \forall y φ$