Metamath Proof Explorer

Theorem 19.40b

Description: The antecedent provides a condition implying the converse of 19.40 . This is to 19.40 what 19.33b is to 19.33 . (Contributed by BJ, 6-May-2019) (Proof shortened by Wolf Lammen, 13-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 pm3.21 ⊢ ψ → φ → φ ∧ ψ
2 1 aleximi ⊢ ∀ x ψ → ∃ x φ → ∃ x φ ∧ ψ
3 pm3.2 ⊢ φ → ψ → φ ∧ ψ
4 3 aleximi ⊢ ∀ x φ → ∃ x ψ → ∃ x φ ∧ ψ
5 2 4 jaoa ⊢ ∀ x ψ ∨ ∀ x φ → ∃ x φ ∧ ∃ x ψ → ∃ x φ ∧ ψ
6 5 orcoms ⊢ ∀ x φ ∨ ∀ x ψ → ∃ x φ ∧ ∃ x ψ → ∃ x φ ∧ ψ
7 19.40 ⊢ ∃ x φ ∧ ψ → ∃ x φ ∧ ∃ x ψ
8 6 7 impbid1 ⊢ ∀ x φ ∨ ∀ x ψ → ∃ x φ ∧ ∃ x ψ ↔ ∃ x φ ∧ ψ