Theorem pm5.18 657

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

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223

This theorem is referenced by:  nbbn 658  pm5.15 663  pm5.16 664  pm5.19 666  dfbi 667  xor3 671

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