Metamath Proof Explorer

Theorem 3orrabdioph

Description: Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion 3orrabdioph ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | χ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ ∈ Dioph ⁡ N

Proof

Step Hyp Ref Expression
1 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
2 1 rabbii ⊢ t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ = t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ
3 orrabdioph ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∈ Dioph ⁡ N
4 orrabdioph ⊢ t ∈ ℕ 0 1 … N | φ ∨ ψ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | χ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ ∈ Dioph ⁡ N
5 3 4 sylan ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | χ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ ∈ Dioph ⁡ N
6 2 5 eqeltrid ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | χ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ ∈ Dioph ⁡ N
7 6 3impa ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | χ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∨ χ ∈ Dioph ⁡ N