Metamath Proof Explorer

Theorem 19.32

Description: Theorem 19.32 of Margaris p. 90. See 19.32v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Revised by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypothesis 19.32.1 ⊢ Ⅎ x φ
Assertion 19.32 ⊢ ∀ x φ ∨ ψ ↔ φ ∨ ∀ x ψ

Proof

Step Hyp Ref Expression
1 19.32.1 ⊢ Ⅎ x φ
2 1 nfn ⊢ Ⅎ x ¬ φ
3 2 19.21 ⊢ ∀ x ¬ φ → ψ ↔ ¬ φ → ∀ x ψ
4 df-or ⊢ φ ∨ ψ ↔ ¬ φ → ψ
5 4 albii ⊢ ∀ x φ ∨ ψ ↔ ∀ x ¬ φ → ψ
6 df-or ⊢ φ ∨ ∀ x ψ ↔ ¬ φ → ∀ x ψ
7 3 5 6 3bitr4i ⊢ ∀ x φ ∨ ψ ↔ φ ∨ ∀ x ψ