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

Metamath Proof Explorer

Theorem 3orel2OLD

Description: Obsolete version of 3orel2 as of 8-Oct-2025. (Contributed by Scott Fenton, 26-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 3orel2OLD ⊢ ¬ ψ → φ ∨ ψ ∨ χ → φ ∨ χ

Proof

Step Hyp Ref Expression
1 3orrot ⊢ φ ∨ ψ ∨ χ ↔ ψ ∨ χ ∨ φ
2 3orel1 ⊢ ¬ ψ → ψ ∨ χ ∨ φ → χ ∨ φ
3 orcom ⊢ χ ∨ φ ↔ φ ∨ χ
4 2 3 imbitrdi ⊢ ¬ ψ → ψ ∨ χ ∨ φ → φ ∨ χ
5 1 4 biimtrid ⊢ ¬ ψ → φ ∨ ψ ∨ χ → φ ∨ χ