Theorem bj-19.12 34205

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

Syntax hints:   → wi 4  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  bj-nnflemae  34208  bj-nnflemea  34209