This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.38b

Description: Under a nonfreeness hypothesis, the implication 19.38 can be strengthened to an equivalence. See also 19.38a . (Contributed by BJ, 3-Nov-2021) (Proof shortened by Wolf Lammen, 9-Jul-2022)

Ref Expression
Assertion 19.38b ( Ⅎ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 19.38 ⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
2 exim ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
3 id ⊢ ( Ⅎ 𝑥 𝜓 → Ⅎ 𝑥 𝜓 )
4 3 nfrd ⊢ ( Ⅎ 𝑥 𝜓 → ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
5 2 4 syl9r ⊢ ( Ⅎ 𝑥 𝜓 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) )
6 1 5 impbid2 ⊢ ( Ⅎ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )