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
|- ( -. ps -> ( ( ph \/ ps \/ ch ) -> ( ph \/ ch ) ) )

Proof

Step Hyp Ref Expression
1 3orrot
 |-  ( ( ph \/ ps \/ ch ) <-> ( ps \/ ch \/ ph ) )
2 3orel1
 |-  ( -. ps -> ( ( ps \/ ch \/ ph ) -> ( ch \/ ph ) ) )
3 orcom
 |-  ( ( ch \/ ph ) <-> ( ph \/ ch ) )
4 2 3 syl6ib
 |-  ( -. ps -> ( ( ps \/ ch \/ ph ) -> ( ph \/ ch ) ) )
5 1 4 syl5bi
 |-  ( -. ps -> ( ( ph \/ ps \/ ch ) -> ( ph \/ ch ) ) )