Metamath Proof Explorer

Theorem pm10.55

Description: Theorem *10.55 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion pm10.55 ⊢ ∃ x φ ∧ ψ ∧ ∀ x φ → ψ ↔ ∃ x φ ∧ ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 exsimpl ⊢ ∃ x φ ∧ ψ → ∃ x φ
2 1 anim1i ⊢ ∃ x φ ∧ ψ ∧ ∀ x φ → ψ → ∃ x φ ∧ ∀ x φ → ψ
3 exintr ⊢ ∀ x φ → ψ → ∃ x φ → ∃ x φ ∧ ψ
4 3 imdistanri ⊢ ∃ x φ ∧ ∀ x φ → ψ → ∃ x φ ∧ ψ ∧ ∀ x φ → ψ
5 2 4 impbii ⊢ ∃ x φ ∧ ψ ∧ ∀ x φ → ψ ↔ ∃ x φ ∧ ∀ x φ → ψ