Theorem axaci

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

	Ref	Expression
Hypothesis	axaci.1	⊢ ( CHOICE ↔ ∀ 𝑥 𝜑 )
Assertion	axaci	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		axaci.1	⊢ ( CHOICE ↔ ∀ 𝑥 𝜑 )
2		axac3	⊢ CHOICE
3	2 1	mpbi	⊢ ∀ 𝑥 𝜑
4	3	spi	⊢ 𝜑