Metamath Proof Explorer

Theorem pm10.541

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

Ref Expression
Assertion pm10.541 ⊢ ∀ 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 φ → ψ
5 df-or ⊢ χ ∨ ψ ↔ ¬ χ → ψ
6 5 imbi2i ⊢ φ → χ ∨ ψ ↔ φ → ¬ χ → ψ
7 6 albii ⊢ ∀ x φ → χ ∨ ψ ↔ ∀ x φ → ¬ χ → ψ
8 df-or ⊢ χ ∨ ∀ x φ → ψ ↔ ¬ χ → ∀ x φ → ψ
9 4 7 8 3bitr4i ⊢ ∀ x φ → χ ∨ ψ ↔ χ ∨ ∀ x φ → ψ