Metamath Proof Explorer

Theorem 19.41rg

Description: Closed form of right-to-left implication of 19.41 , Theorem 19.41 of Margaris p. 90. Derived from 19.41rgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.41rg ⊢ ∀ x ψ → ∀ x ψ → ∃ x φ ∧ ψ → ∃ x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 sp ⊢ ∀ x ψ → ∀ x ψ → ψ → ∀ x ψ
2 pm3.21 ⊢ ψ → φ → φ ∧ ψ
3 2 a1i ⊢ ψ → ∀ x ψ → ψ → φ → φ ∧ ψ
4 3 al2imi ⊢ ∀ x ψ → ∀ x ψ → ∀ x ψ → ∀ x φ → φ ∧ ψ
5 exim ⊢ ∀ x φ → φ ∧ ψ → ∃ x φ → ∃ x φ ∧ ψ
6 4 5 syl6 ⊢ ∀ x ψ → ∀ x ψ → ∀ x ψ → ∃ x φ → ∃ x φ ∧ ψ
7 1 6 syld ⊢ ∀ x ψ → ∀ x ψ → ψ → ∃ x φ → ∃ x φ ∧ ψ
8 7 com23 ⊢ ∀ x ψ → ∀ x ψ → ∃ x φ → ψ → ∃ x φ ∧ ψ
9 8 impd ⊢ ∀ x ψ → ∀ x ψ → ∃ x φ ∧ ψ → ∃ x φ ∧ ψ