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	|- ((ph <-> ps) <-> -. (ph <-> -. ps))

Proof of Theorem pm5.18

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

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