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

Metamath Proof Explorer

Theorem axaci

Description: Apply a choice equivalent. (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Hypothesis	axaci.1	$⊢ CHOICE \leftrightarrow \forall x φ$
	Assertion	axaci	$⊢ φ$

Step	Hyp	Ref	Expression
1		axaci.1	$⊢ CHOICE \leftrightarrow \forall x φ$
2		axac3	$⊢ CHOICE$
3	2 1	mpbi	$⊢ \forall x φ$
4	3	spi	$⊢ φ$