Metamath Proof Explorer

Theorem 3r19.43

Description: Restricted quantifier version of 19.43 for a triple disjunction . (Contributed by AV, 2-Nov-2025)

Ref Expression
Assertion 3r19.43 ⊢ ∃ x ∈ A φ ∨ ψ ∨ χ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ

Proof

Step Hyp Ref Expression
1 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
2 1 rexbii ⊢ ∃ x ∈ A φ ∨ ψ ∨ χ ↔ ∃ x ∈ A φ ∨ ψ ∨ χ
3 r19.43 ⊢ ∃ x ∈ A φ ∨ ψ ∨ χ ↔ ∃ x ∈ A φ ∨ ψ ∨ ∃ x ∈ A χ
4 r19.43 ⊢ ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ
5 4 orbi1i ⊢ ∃ x ∈ A φ ∨ ψ ∨ ∃ x ∈ A χ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ
6 df-3or ⊢ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ
7 5 6 bitr4i ⊢ ∃ x ∈ A φ ∨ ψ ∨ ∃ x ∈ A χ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ
8 2 3 7 3bitri ⊢ ∃ x ∈ A φ ∨ ψ ∨ χ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ ∨ ∃ x ∈ A χ