Metamath Proof Explorer

Theorem pm10.542

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

Ref Expression
Assertion pm10.542 ⊢ ∀ x φ → χ → ψ ↔ χ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 bi2.04 ⊢ φ → χ → ψ ↔ χ → φ → ψ
2 1 albii ⊢ ∀ x φ → χ → ψ ↔ ∀ x χ → φ → ψ
3 19.21v ⊢ ∀ x χ → φ → ψ ↔ χ → ∀ x φ → ψ
4 2 3 bitri ⊢ ∀ x φ → χ → ψ ↔ χ → ∀ x φ → ψ