Theorem pm5.75 952

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 462	. . 3 ⊢ ((𝜑 ↔ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) ↔ ((𝜓 ∨ 𝜒) ∧ ¬ 𝜓)))
2		orcom 718	. . . . 5 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	2	anbi1i 454	. . . 4 ⊢ (((𝜓 ∨ 𝜒) ∧ ¬ 𝜓) ↔ ((𝜒 ∨ 𝜓) ∧ ¬ 𝜓))
4		pm5.61 784	. . . 4 ⊢ (((𝜒 ∨ 𝜓) ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓))
5	3, 4	bitri 183	. . 3 ⊢ (((𝜓 ∨ 𝜒) ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓))
6	1, 5	bitrdi 195	. 2 ⊢ ((𝜑 ↔ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) ↔ (𝜒 ∧ ¬ 𝜓)))
7		pm4.71 387	. . . 4 ⊢ ((𝜒 → ¬ 𝜓) ↔ (𝜒 ↔ (𝜒 ∧ ¬ 𝜓)))
8	7	biimpi 119	. . 3 ⊢ ((𝜒 → ¬ 𝜓) → (𝜒 ↔ (𝜒 ∧ ¬ 𝜓)))
9	8	bicomd 140	. 2 ⊢ ((𝜒 → ¬ 𝜓) → ((𝜒 ∧ ¬ 𝜓) ↔ 𝜒))
10	6, 9	sylan9bbr 459	1 ⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by: (None)