Metamath Proof Explorer

Theorem 19.33b

Description: The antecedent provides a condition implying the converse of 19.33 . (Contributed by NM, 27-Mar-2004) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 5-Jul-2014)

Ref Expression
Assertion 19.33b ⊢ ¬ ∃ x φ ∧ ∃ x ψ → ∀ x φ ∨ ψ ↔ ∀ x φ ∨ ∀ x ψ

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ ∃ x φ ∧ ∃ x ψ ↔ ¬ ∃ x φ ∨ ¬ ∃ x ψ
2 alnex ⊢ ∀ x ¬ φ ↔ ¬ ∃ x φ
3 pm2.53 ⊢ φ ∨ ψ → ¬ φ → ψ
4 3 al2imi ⊢ ∀ x φ ∨ ψ → ∀ x ¬ φ → ∀ x ψ
5 2 4 biimtrrid ⊢ ∀ x φ ∨ ψ → ¬ ∃ x φ → ∀ x ψ
6 olc ⊢ ∀ x ψ → ∀ x φ ∨ ∀ x ψ
7 5 6 syl6com ⊢ ¬ ∃ x φ → ∀ x φ ∨ ψ → ∀ x φ ∨ ∀ x ψ
8 19.30 ⊢ ∀ x φ ∨ ψ → ∀ x φ ∨ ∃ x ψ
9 8 orcomd ⊢ ∀ x φ ∨ ψ → ∃ x ψ ∨ ∀ x φ
10 9 ord ⊢ ∀ x φ ∨ ψ → ¬ ∃ x ψ → ∀ x φ
11 orc ⊢ ∀ x φ → ∀ x φ ∨ ∀ x ψ
12 10 11 syl6com ⊢ ¬ ∃ x ψ → ∀ x φ ∨ ψ → ∀ x φ ∨ ∀ x ψ
13 7 12 jaoi ⊢ ¬ ∃ x φ ∨ ¬ ∃ x ψ → ∀ x φ ∨ ψ → ∀ x φ ∨ ∀ x ψ
14 1 13 sylbi ⊢ ¬ ∃ x φ ∧ ∃ x ψ → ∀ x φ ∨ ψ → ∀ x φ ∨ ∀ x ψ
15 19.33 ⊢ ∀ x φ ∨ ∀ x ψ → ∀ x φ ∨ ψ
16 14 15 impbid1 ⊢ ¬ ∃ x φ ∧ ∃ x ψ → ∀ x φ ∨ ψ ↔ ∀ x φ ∨ ∀ x ψ