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 ¬ ψ φ ψ χ φ χ