This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ψ → θ