Theorem bj-19.12 36756

Description: See 19.12 2326. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2163 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1784 or df-bj-nnf 36719, 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 36683	. 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑)
2		excom 2163	. . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑)
3		axc7e 2317	. . . 4 ⊢ (∃𝑦∀𝑦𝜑 → 𝜑)
4	3	eximi 1835	. . 3 ⊢ (∃𝑥∃𝑦∀𝑦𝜑 → ∃𝑥𝜑)
5	2, 4	sylbi 217	. 2 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 → ∃𝑥𝜑)
6	1, 5	sylg 1823	1 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  bj-nnflemae  36759  bj-nnflemea  36760