Theorem pm5.18 497

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 398	. 2 ⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))
2		bicom 398	. . . 4 ⊢ ((φ ↔ ¬ ψ) ↔ (¬ ψ ↔ φ))
3		pm2.61 109	. . . . . . . . . . 11 ⊢ ((ψ → φ) → ((¬ ψ → φ) → φ))
4		pm2.65 115	. . . . . . . . . . . 12 ⊢ ((ψ → φ) → ((ψ → ¬ φ) → ¬ ψ))
5		con2 82	. . . . . . . . . . . 12 ⊢ ((φ → ¬ ψ) → (ψ → ¬ φ))
6	4, 5	syl5 22	. . . . . . . . . . 11 ⊢ ((ψ → φ) → ((φ → ¬ ψ) → ¬ ψ))
7	3, 6	anim12d 431	. . . . . . . . . 10 ⊢ ((ψ → φ) → (((¬ ψ → φ) ∧ (φ → ¬ ψ)) → (φ ∧ ¬ ψ)))
8		bi 396	. . . . . . . . . 10 ⊢ ((¬ ψ ↔ φ) ↔ ((¬ ψ → φ) ∧ (φ → ¬ ψ)))
9	7, 8	syl5ib 181	. . . . . . . . 9 ⊢ ((ψ → φ) → ((¬ ψ ↔ φ) → (φ ∧ ¬ ψ)))
10		annim 206	. . . . . . . . 9 ⊢ ((φ ∧ ¬ ψ) ↔ ¬ (φ → ψ))
11	9, 10	syl6ib 185	. . . . . . . 8 ⊢ ((ψ → φ) → ((¬ ψ ↔ φ) → ¬ (φ → ψ)))
12	11	com12 13	. . . . . . 7 ⊢ ((¬ ψ ↔ φ) → ((ψ → φ) → ¬ (φ → ψ)))
13		imnan 207	. . . . . . 7 ⊢ (((ψ → φ) → ¬ (φ → ψ)) ↔ ¬ ((ψ → φ) ∧ (φ → ψ)))
14	12, 13	sylib 173	. . . . . 6 ⊢ ((¬ ψ ↔ φ) → ¬ ((ψ → φ) ∧ (φ → ψ)))
15		bi 396	. . . . . . 7 ⊢ ((ψ ↔ φ) ↔ ((ψ → φ) ∧ (φ → ψ)))
16	15	negbii 162	. . . . . 6 ⊢ (¬ (ψ ↔ φ) ↔ ¬ ((ψ → φ) ∧ (φ → ψ)))
17	14, 16	sylibr 175	. . . . 5 ⊢ ((¬ ψ ↔ φ) → ¬ (ψ ↔ φ))
18		pm2.24 72	. . . . . . . . . 10 ⊢ (ψ → (¬ ψ → φ))
19		pm2.21 71	. . . . . . . . . 10 ⊢ (¬ ψ → (ψ → φ))
20	18, 19	nsyl4 105	. . . . . . . . 9 ⊢ (¬ (ψ → φ) → (¬ ψ → φ))
21		annim 206	. . . . . . . . . 10 ⊢ ((ψ ∧ ¬ φ) ↔ ¬ (ψ → φ))
22		pm2.21 71	. . . . . . . . . . 11 ⊢ (¬ φ → (φ → ¬ ψ))
23	22	adantl 305	. . . . . . . . . 10 ⊢ ((ψ ∧ ¬ φ) → (φ → ¬ ψ))
24	21, 23	sylbir 176	. . . . . . . . 9 ⊢ (¬ (ψ → φ) → (φ → ¬ ψ))
25	20, 24	jca 236	. . . . . . . 8 ⊢ (¬ (ψ → φ) → ((¬ ψ → φ) ∧ (φ → ¬ ψ)))
26		ax-1 3	. . . . . . . . . . 11 ⊢ (φ → (¬ ψ → φ))
27	26	adantr 306	. . . . . . . . . 10 ⊢ ((φ ∧ ¬ ψ) → (¬ ψ → φ))
28	10, 27	sylbir 176	. . . . . . . . 9 ⊢ (¬ (φ → ψ) → (¬ ψ → φ))
29		pm3.4 266	. . . . . . . . . 10 ⊢ ((φ ∧ ¬ ψ) → (φ → ¬ ψ))
30	10, 29	sylbir 176	. . . . . . . . 9 ⊢ (¬ (φ → ψ) → (φ → ¬ ψ))
31	28, 30	jca 236	. . . . . . . 8 ⊢ (¬ (φ → ψ) → ((¬ ψ → φ) ∧ (φ → ¬ ψ)))
32	25, 31	jaoi 275	. . . . . . 7 ⊢ ((¬ (ψ → φ) ∨ ¬ (φ → ψ)) → ((¬ ψ → φ) ∧ (φ → ¬ ψ)))
33		ianor 253	. . . . . . 7 ⊢ (¬ ((ψ → φ) ∧ (φ → ψ)) ↔ (¬ (ψ → φ) ∨ ¬ (φ → ψ)))
34	32, 33, 8	3imtr4 192	. . . . . 6 ⊢ (¬ ((ψ → φ) ∧ (φ → ψ)) → (¬ ψ ↔ φ))
35	16, 34	sylbi 174	. . . . 5 ⊢ (¬ (ψ ↔ φ) → (¬ ψ ↔ φ))
36	17, 35	impbi 139	. . . 4 ⊢ ((¬ ψ ↔ φ) ↔ ¬ (ψ ↔ φ))
37	2, 36	bitr 151	. . 3 ⊢ ((φ ↔ ¬ ψ) ↔ ¬ (ψ ↔ φ))
38	37	bicon2i 194	. 2 ⊢ ((ψ ↔ φ) ↔ ¬ (φ ↔ ¬ ψ))
39	1, 38	bitr 151	1 ⊢ ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  nbbn 498  dfbi 499  ru 1437  sbc2or 1454

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org