Metamath Proof Explorer

Theorem ts3or1

Description: A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018)

Ref Expression
Assertion ts3or1 ⊢ θ → φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 exmidd ⊢ θ → φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ψ ∨ χ
2 df-3or ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ
3 2 notbii ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ ∨ χ
4 3 orbi2i ⊢ φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ψ ∨ χ
5 1 4 sylibr ⊢ θ → φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ψ ∨ χ