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

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 ⊢ ( ( ( 𝜒 → ¬ 𝜓 ) ∧ ( 𝜑 ↔ ( 𝜓 ∨ 𝜒 ) ) ) → ( ( 𝜑 ∧ ¬ 𝜓 ) ↔ 𝜒 ) )