Metamath Proof Explorer

Theorem cases

Description: Case disjunction according to the value of ph . (Contributed by NM, 25-Apr-2019)

Ref Expression
Hypotheses cases.1 ⊢ φ → ψ ↔ χ
cases.2 ⊢ ¬ φ → ψ ↔ θ
Assertion cases ⊢ ψ ↔ φ ∧ χ ∨ ¬ φ ∧ θ

Proof

Step Hyp Ref Expression
1 cases.1 ⊢ φ → ψ ↔ χ
2 cases.2 ⊢ ¬ φ → ψ ↔ θ
3 exmid ⊢ φ ∨ ¬ φ
4 3 biantrur ⊢ ψ ↔ φ ∨ ¬ φ ∧ ψ
5 andir ⊢ φ ∨ ¬ φ ∧ ψ ↔ φ ∧ ψ ∨ ¬ φ ∧ ψ
6 1 pm5.32i ⊢ φ ∧ ψ ↔ φ ∧ χ
7 2 pm5.32i ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∧ θ
8 6 7 orbi12i ⊢ φ ∧ ψ ∨ ¬ φ ∧ ψ ↔ φ ∧ χ ∨ ¬ φ ∧ θ
9 4 5 8 3bitri ⊢ ψ ↔ φ ∧ χ ∨ ¬ φ ∧ θ