Theorem 3o3cs

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

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