Metamath Proof Explorer


Theorem axie2

Description: A key property of existential quantification (intuitionistic logic axiom ax-ie2). (Contributed by Jim Kingdon, 31-Dec-2017)

Ref Expression
Assertion axie2 ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 nf5 ( Ⅎ 𝑥 𝜓 ↔ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) )
2 19.23t ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) ) )
3 1 2 sylbir ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ∀ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) ) )