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

Metamath Proof Explorer

Theorem 19.29r

Description: Variation of 19.29 . (Contributed by NM, 18-Aug-1993) (Proof shortened by Wolf Lammen, 12-Nov-2020)

Ref Expression
Assertion 19.29r ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 pm3.21 ⊢ ψ → φ → φ ∧ ψ
2 1 aleximi ⊢ ∀ x ψ → ∃ x φ → ∃ x φ ∧ ψ
3 2 impcom ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ψ