Theorem bj-19.12 37162

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

Syntax hints:   → wi 4  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  bj-nnflemae  37227  bj-nnflemea  37228