Metamath Proof Explorer


Theorem 3o3cs

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

Ref Expression
Hypothesis 3o1cs.1 ( ( 𝜑𝜓𝜒 ) → 𝜃 )
Assertion 3o3cs ( 𝜒𝜃 )

Proof

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