Theorem bj-modal5e 31825

Description: Dual statement of hbe1 2008 (which is the real modal-5 2019). See also axc7 2117 and axc7e 2118. (Contributed by BJ, 21-Dec-2020.)

Assertion

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

Proof of Theorem bj-modal5e

Step	Hyp	Ref	Expression
1		hbn1 2007	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
2		alnex 1697	. . 3 ⊢ (∀𝑥 ¬ ∀𝑥𝜑 ↔ ¬ ∃𝑥∀𝑥𝜑)
3	1, 2	sylib 207	. 2 ⊢ (¬ ∀𝑥𝜑 → ¬ ∃𝑥∀𝑥𝜑)
4	3	con4i 112	1 ⊢ (∃𝑥∀𝑥𝜑 → ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  bj-19.41al  31826  bj-sb56  31828