Theorem 3o2cs

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

	Ref	Expression
Hypothesis	3o1cs.1	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) → 𝜃 )
Assertion	3o2cs	⊢ ( 𝜓 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		3o1cs.1	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) → 𝜃 )
2		df-3or	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
3	2 1	sylbir	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → 𝜃 )
4	3	orcs	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜃 )
5	4	olcs	⊢ ( 𝜓 → 𝜃 )