Theorem pm5.18 658

Description: Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive-or."

Assertion

Ref	Expression
pm5.18	⊢ ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))

Proof of Theorem pm5.18

Step	Hyp	Ref	Expression
1		bicom 518	. 2 ⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))
2		bicom 518	. . . 4 ⊢ ((φ ↔ ¬ ψ) ↔ (¬ ψ ↔ φ))
3		pm2.61 124	. . . . . . . . . . 11 ⊢ ((ψ → φ) → ((¬ ψ → φ) → φ))
4		pm2.65 134	. . . . . . . . . . . 12 ⊢ ((ψ → φ) → ((ψ → ¬ φ) → ¬ ψ))
5		con2 90	. . . . . . . . . . . 12 ⊢ ((φ → ¬ ψ) → (ψ → ¬ φ))
6	4, 5	syl5 21	. . . . . . . . . . 11 ⊢ ((ψ → φ) → ((φ → ¬ ψ) → ¬ ψ))
7	3, 6	anim12d 556	. . . . . . . . . 10 ⊢ ((ψ → φ) → (((¬ ψ → φ) ⋀ (φ → ¬ ψ)) → (φ ⋀ ¬ ψ)))
8		bi 513	. . . . . . . . . 10 ⊢ ((¬ ψ ↔ φ) ↔ ((¬ ψ → φ) ⋀ (φ → ¬ ψ)))
9	7, 8	syl5ib 206	. . . . . . . . 9 ⊢ ((ψ → φ) → ((¬ ψ ↔ φ) → (φ ⋀ ¬ ψ)))
10		annim 238	. . . . . . . . 9 ⊢ ((φ ⋀ ¬ ψ) ↔ ¬ (φ → ψ))
11	9, 10	syl6ib 212	. . . . . . . 8 ⊢ ((ψ → φ) → ((¬ ψ ↔ φ) → ¬ (φ → ψ)))
12	11	com12 11	. . . . . . 7 ⊢ ((¬ ψ ↔ φ) → ((ψ → φ) → ¬ (φ → ψ)))
13		imnan 242	. . . . . . 7 ⊢ (((ψ → φ) → ¬ (φ → ψ)) ↔ ¬ ((ψ → φ) ⋀ (φ → ψ)))
14	12, 13	sylib 198	. . . . . 6 ⊢ ((¬ ψ ↔ φ) → ¬ ((ψ → φ) ⋀ (φ → ψ)))
15		bi 513	. . . . . . 7 ⊢ ((ψ ↔ φ) ↔ ((ψ → φ) ⋀ (φ → ψ)))
16	15	negbii 187	. . . . . 6 ⊢ (¬ (ψ ↔ φ) ↔ ¬ ((ψ → φ) ⋀ (φ → ψ)))
17	14, 16	sylibr 200	. . . . 5 ⊢ ((¬ ψ ↔ φ) → ¬ (ψ ↔ φ))
18		pm2.5 100	. . . . . . . . 9 ⊢ (¬ (ψ → φ) → (¬ ψ → φ))
19		annim 238	. . . . . . . . . 10 ⊢ ((ψ ⋀ ¬ φ) ↔ ¬ (ψ → φ))
20		pm2.21 76	. . . . . . . . . . 11 ⊢ (¬ φ → (φ → ¬ ψ))
21	20	adantl 388	. . . . . . . . . 10 ⊢ ((ψ ⋀ ¬ φ) → (φ → ¬ ψ))
22	19, 21	sylbir 201	. . . . . . . . 9 ⊢ (¬ (ψ → φ) → (φ → ¬ ψ))
23	18, 22	jca 288	. . . . . . . 8 ⊢ (¬ (ψ → φ) → ((¬ ψ → φ) ⋀ (φ → ¬ ψ)))
24		ax-1 4	. . . . . . . . . . 11 ⊢ (φ → (¬ ψ → φ))
25	24	adantr 389	. . . . . . . . . 10 ⊢ ((φ ⋀ ¬ ψ) → (¬ ψ → φ))
26	10, 25	sylbir 201	. . . . . . . . 9 ⊢ (¬ (φ → ψ) → (¬ ψ → φ))
27		pm2.51 101	. . . . . . . . 9 ⊢ (¬ (φ → ψ) → (φ → ¬ ψ))
28	26, 27	jca 288	. . . . . . . 8 ⊢ (¬ (φ → ψ) → ((¬ ψ → φ) ⋀ (φ → ¬ ψ)))
29	23, 28	jaoi 341	. . . . . . 7 ⊢ ((¬ (ψ → φ) ⋁ ¬ (φ → ψ)) → ((¬ ψ → φ) ⋀ (φ → ¬ ψ)))
30		ianor 305	. . . . . . 7 ⊢ (¬ ((ψ → φ) ⋀ (φ → ψ)) ↔ (¬ (ψ → φ) ⋁ ¬ (φ → ψ)))
31	29, 30, 8	3imtr4 219	. . . . . 6 ⊢ (¬ ((ψ → φ) ⋀ (φ → ψ)) → (¬ ψ ↔ φ))
32	16, 31	sylbi 199	. . . . 5 ⊢ (¬ (ψ ↔ φ) → (¬ ψ ↔ φ))
33	17, 32	impbi 157	. . . 4 ⊢ ((¬ ψ ↔ φ) ↔ ¬ (ψ ↔ φ))
34	2, 33	bitr 173	. . 3 ⊢ ((φ ↔ ¬ ψ) ↔ ¬ (ψ ↔ φ))
35	34	con2bii 221	. 2 ⊢ ((ψ ↔ φ) ↔ ¬ (φ ↔ ¬ ψ))
36	1, 35	bitr 173	1 ⊢ ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223

This theorem is referenced by:  nbbn 659  pm5.15 664  pm5.16 665  pm5.19 667  dfbi 668  xor3 672

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain