Metamath Proof Explorer


Theorem 3orel2

Description: Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Assertion 3orel2 ( ¬ 𝜓 → ( ( 𝜑𝜓𝜒 ) → ( 𝜑𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 3orrot ( ( 𝜑𝜓𝜒 ) ↔ ( 𝜓𝜒𝜑 ) )
2 3orel1 ( ¬ 𝜓 → ( ( 𝜓𝜒𝜑 ) → ( 𝜒𝜑 ) ) )
3 orcom ( ( 𝜒𝜑 ) ↔ ( 𝜑𝜒 ) )
4 2 3 syl6ib ( ¬ 𝜓 → ( ( 𝜓𝜒𝜑 ) → ( 𝜑𝜒 ) ) )
5 1 4 syl5bi ( ¬ 𝜓 → ( ( 𝜑𝜓𝜒 ) → ( 𝜑𝜒 ) ) )