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)

Ref Expression
Assertion 3orel2 ¬ψφψχφχ

Proof

Step Hyp Ref Expression
1 3orrot φψχψχφ
2 3orel1 ¬ψψχφχφ
3 orcom χφφχ
4 2 3 syl6ib ¬ψψχφφχ
5 1 4 syl5bi ¬ψφψχφχ