Theorem bj-19.12 37389

Description: See 19.12 2363. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2200 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1817 or df-bj-nnf 37393, directly or indirectly. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-19.12	⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)

Proof of Theorem bj-19.12

Step	Hyp	Ref	Expression
1		bj-modalbe 37354	. 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑)
2		excom 2200	. . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑)
3		axc7e 2354	. . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑)
4	3	eximi 1868	. . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑)
5	2, 4	sylbi 220	. 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑)
6	1, 5	sylg 1856	1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  bj-nnflemae  37454  bj-nnflemea  37455