Metamath Proof Explorer


Theorem 19.2d

Description: Deduction associated with 19.2 . (Contributed by BJ, 12-May-2019)

Ref Expression
Hypothesis 19.2d.1 ⊢ φ → ∀ x ψ
Assertion 19.2d ⊢ φ → ∃ x ψ

Proof

Step Hyp Ref Expression
1 19.2d.1 ⊢ φ → ∀ x ψ
2 19.2 ⊢ ∀ x ψ → ∃ x ψ
3 1 2 syl ⊢ φ → ∃ x ψ