This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3orel2

Description: Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Eric Schmidt, 8-Oct-2025)

Ref Expression
Assertion 3orel2 ⊢ ¬ ψ → φ ∨ ψ ∨ χ → φ ∨ χ

Proof

Step Hyp Ref Expression
1 3orcoma ⊢ φ ∨ ψ ∨ χ ↔ ψ ∨ φ ∨ χ
2 3orel1 ⊢ ¬ ψ → ψ ∨ φ ∨ χ → φ ∨ χ
3 1 2 biimtrid ⊢ ¬ ψ → φ ∨ ψ ∨ χ → φ ∨ χ