Metamath Proof Explorer


Theorem 3o1cs

Description: Deduction eliminating disjunct. (Contributed by Thierry Arnoux, 19-Dec-2016)

Ref Expression
Hypothesis 3o1cs.1
|- ( ( ph \/ ps \/ ch ) -> th )
Assertion 3o1cs
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 3o1cs.1
 |-  ( ( ph \/ ps \/ ch ) -> th )
2 df-3or
 |-  ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
3 2 1 sylbir
 |-  ( ( ( ph \/ ps ) \/ ch ) -> th )
4 3 orcs
 |-  ( ( ph \/ ps ) -> th )
5 4 orcs
 |-  ( ph -> th )