Theorem pm5.75 962

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.)

Assertion

Ref	Expression
pm5.75	⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒))

Proof of Theorem pm5.75

Step	Hyp	Ref	Expression
1		anbi1 466	. . 3 ⊢ ((𝜑 ↔ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) ↔ ((𝜓 ∨ 𝜒) ∧ ¬ 𝜓)))
2		orcom 728	. . . . 5 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	2	anbi1i 458	. . . 4 ⊢ (((𝜓 ∨ 𝜒) ∧ ¬ 𝜓) ↔ ((𝜒 ∨ 𝜓) ∧ ¬ 𝜓))
4		pm5.61 794	. . . 4 ⊢ (((𝜒 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓))
5	3, 4	bitri 184	. . 3 ⊢ (((𝜓 ∨ 𝜒) ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓))
6	1, 5	bitrdi 196	. 2 ⊢ ((𝜑 ↔ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓)))
7		pm4.71 389	. . . 4 ⊢ ((𝜒 → ¬ 𝜓) ↔ (𝜒 ↔ (𝜒 ∧ ¬ 𝜓)))
8	7	biimpi 120	. . 3 ⊢ ((𝜒 → ¬ 𝜓) → (𝜒 ↔ (𝜒 ∧ ¬ 𝜓)))
9	8	bicomd 141	. 2 ⊢ ((𝜒 → ¬ 𝜓) → ((𝜒 ∧ ¬ 𝜓) ↔ 𝜒))
10	6, 9	sylan9bbr 463	1 ⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by: (None)