Theorem bj-alcomexcom

Description: Commutation of universal quantifiers implies commutation of existential quantifiers. Can be placed in the ax-4 section, soon after 2nexaln , and used to prove excom . (Contributed by BJ, 29-Nov-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-alcomexcom	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) → ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		2nexaln	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
2		2nexaln	⊢ ( ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 )
3	1 2	imbi12i	⊢ ( ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 → ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) )
4		con4	⊢ ( ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 → ¬ ∃ 𝑦 ∃ 𝑥 𝜑 ) → ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) )
5	3 4	sylbir	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) → ( ∃ 𝑦 ∃ 𝑥 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜑 ) )