Metamath Proof Explorer

Theorem pm11.59

Description: Theorem *11.59 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion pm11.59 ⊢ ∀ x φ → ψ → ∀ y ∀ x φ ∧ y x φ → ψ ∧ y x ψ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y φ → ψ
2 1 nfal ⊢ Ⅎ y ∀ x φ → ψ
3 sp ⊢ ∀ x φ → ψ → φ → ψ
4 spsbim ⊢ ∀ x φ → ψ → y x φ → y x ψ
5 3 4 anim12d ⊢ ∀ x φ → ψ → φ ∧ y x φ → ψ ∧ y x ψ
6 5 axc4i ⊢ ∀ x φ → ψ → ∀ x φ ∧ y x φ → ψ ∧ y x ψ
7 2 6 alrimi ⊢ ∀ x φ → ψ → ∀ y ∀ x φ ∧ y x φ → ψ ∧ y x ψ