Theorem axaci

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

	Ref	Expression
Hypothesis	axaci.1	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\phi$$
Assertion	axaci	$$⊢\phi$$

Proof

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