Metamath Proof Explorer

Theorem pm5.75

Description: Theorem *5.75 of WhiteheadRussell p. 126. (Contributed by NM, 3-Jan-2005) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 23-Dec-2012) (Proof shortened by Kyle Wyonch, 12-Feb-2021)

Ref Expression
Assertion pm5.75 ⊢ χ → ¬ ψ ∧ φ ↔ ψ ∨ χ → φ ∧ ¬ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 anbi1 ⊢ φ ↔ ψ ∨ χ → φ ∧ ¬ ψ ↔ ψ ∨ χ ∧ ¬ ψ
2 biorf ⊢ ¬ ψ → χ ↔ ψ ∨ χ
3 2 bicomd ⊢ ¬ ψ → ψ ∨ χ ↔ χ
4 3 pm5.32ri ⊢ ψ ∨ χ ∧ ¬ ψ ↔ χ ∧ ¬ ψ
5 1 4 bitrdi ⊢ φ ↔ ψ ∨ χ → φ ∧ ¬ ψ ↔ χ ∧ ¬ ψ
6 abai ⊢ χ ∧ ¬ ψ ↔ χ ∧ χ → ¬ ψ
7 6 rbaib ⊢ χ → ¬ ψ → χ ∧ ¬ ψ ↔ χ
8 5 7 sylan9bbr ⊢ χ → ¬ ψ ∧ φ ↔ ψ ∨ χ → φ ∧ ¬ ψ ↔ χ