Metamath Proof Explorer

Theorem cases2

Description: Case disjunction according to the value of ph . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 28-Feb-2022)

Ref Expression
Assertion cases2 ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ → ψ ∧ ¬ φ → χ

Proof

Step Hyp Ref Expression
1 pm4.83 ⊢ φ → ψ ∧ φ ∨ χ ∧ ¬ φ ∧ ¬ φ → ψ ∧ φ ∨ χ ∧ ¬ φ ↔ ψ ∧ φ ∨ χ ∧ ¬ φ
2 dedlema ⊢ φ → ψ ↔ ψ ∧ φ ∨ χ ∧ ¬ φ
3 2 pm5.74i ⊢ φ → ψ ↔ φ → ψ ∧ φ ∨ χ ∧ ¬ φ
4 dedlemb ⊢ ¬ φ → χ ↔ ψ ∧ φ ∨ χ ∧ ¬ φ
5 4 pm5.74i ⊢ ¬ φ → χ ↔ ¬ φ → ψ ∧ φ ∨ χ ∧ ¬ φ
6 3 5 anbi12i ⊢ φ → ψ ∧ ¬ φ → χ ↔ φ → ψ ∧ φ ∨ χ ∧ ¬ φ ∧ ¬ φ → ψ ∧ φ ∨ χ ∧ ¬ φ
7 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
8 ancom ⊢ ¬ φ ∧ χ ↔ χ ∧ ¬ φ
9 7 8 orbi12i ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ ψ ∧ φ ∨ χ ∧ ¬ φ
10 1 6 9 3bitr4ri ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ → ψ ∧ ¬ φ → χ