Theorem 3o2cs

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

	Ref	Expression
Hypothesis	3o1cs.1	|- ( ( ph \/ ps \/ ch ) -> th )
Assertion	3o2cs	|- ( ps -> 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	olcs	|- ( ps -> th )