Theorem bj-19.12 36762

Description: See 19.12 2327. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2162 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 36725, 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 36689	. 2 ⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑦∃𝑥∀𝑦𝜑)
2		excom 2162	. . 3 ⊢ (∃𝑦∃𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦∀𝑦𝜑)
3		axc7e 2318	. . . 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 2007  ax-10 2141  ax-11 2157  ax-12 2177

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

This theorem is referenced by:  bj-nnflemae  36765  bj-nnflemea  36766