Theorem pm5.18OLD 723

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

Proof of Theorem pm5.18OLD

Step	Hyp	Ref	Expression
1		bicom 579	. 2 |- ((ph <-> ps) <-> (ps <-> ph))
2		bicom 579	. . . 4 |- ((ph <-> -. ps) <-> (-. ps <-> ph))
3		pm2.61 139	. . . . . . . . . . 11 |- ((ps -> ph) -> ((-. ps -> ph) -> ph))
4		pm2.65 149	. . . . . . . . . . . 12 |- ((ps -> ph) -> ((ps -> -. ph) -> -. ps))
5		con2 106	. . . . . . . . . . . 12 |- ((ph -> -. ps) -> (ps -> -. ph))
6	4, 5	syl5 20	. . . . . . . . . . 11 |- ((ps -> ph) -> ((ph -> -. ps) -> -. ps))
7	3, 6	anim12d 617	. . . . . . . . . 10 |- ((ps -> ph) -> (((-. ps -> ph) /\ (ph -> -. ps)) -> (ph /\ -. ps)))
8		dfbi2 572	. . . . . . . . . 10 |- ((-. ps <-> ph) <-> ((-. ps -> ph) /\ (ph -> -. ps)))
9	7, 8	syl5ib 223	. . . . . . . . 9 |- ((ps -> ph) -> ((-. ps <-> ph) -> (ph /\ -. ps)))
10		annim 257	. . . . . . . . 9 |- ((ph /\ -. ps) <-> -. (ph -> ps))
11	9, 10	syl6ib 229	. . . . . . . 8 |- ((ps -> ph) -> ((-. ps <-> ph) -> -. (ph -> ps)))
12	11	com12 14	. . . . . . 7 |- ((-. ps <-> ph) -> ((ps -> ph) -> -. (ph -> ps)))
13		imnan 261	. . . . . . 7 |- (((ps -> ph) -> -. (ph -> ps)) <-> -. ((ps -> ph) /\ (ph -> ps)))
14	12, 13	sylib 215	. . . . . 6 |- ((-. ps <-> ph) -> -. ((ps -> ph) /\ (ph -> ps)))
15		dfbi2 572	. . . . . . 7 |- ((ps <-> ph) <-> ((ps -> ph) /\ (ph -> ps)))
16	15	notbii 204	. . . . . 6 |- (-. (ps <-> ph) <-> -. ((ps -> ph) /\ (ph -> ps)))
17	14, 16	sylibr 217	. . . . 5 |- ((-. ps <-> ph) -> -. (ps <-> ph))
18		pm2.5 115	. . . . . . . . 9 |- (-. (ps -> ph) -> (-. ps -> ph))
19		annim 257	. . . . . . . . . 10 |- ((ps /\ -. ph) <-> -. (ps -> ph))
20		pm2.21 92	. . . . . . . . . . 11 |- (-. ph -> (ph -> -. ps))
21	20	adantl 424	. . . . . . . . . 10 |- ((ps /\ -. ph) -> (ph -> -. ps))
22	19, 21	sylbir 218	. . . . . . . . 9 |- (-. (ps -> ph) -> (ph -> -. ps))
23	18, 22	jca 310	. . . . . . . 8 |- (-. (ps -> ph) -> ((-. ps -> ph) /\ (ph -> -. ps)))
24		ax-1 4	. . . . . . . . . . 11 |- (ph -> (-. ps -> ph))
25	24	adantr 425	. . . . . . . . . 10 |- ((ph /\ -. ps) -> (-. ps -> ph))
26	10, 25	sylbir 218	. . . . . . . . 9 |- (-. (ph -> ps) -> (-. ps -> ph))
27		pm2.51 116	. . . . . . . . 9 |- (-. (ph -> ps) -> (ph -> -. ps))
28	26, 27	jca 310	. . . . . . . 8 |- (-. (ph -> ps) -> ((-. ps -> ph) /\ (ph -> -. ps)))
29	23, 28	jaoi 368	. . . . . . 7 |- ((-. (ps -> ph) \/ -. (ph -> ps)) -> ((-. ps -> ph) /\ (ph -> -. ps)))
30		ianor 329	. . . . . . 7 |- (-. ((ps -> ph) /\ (ph -> ps)) <-> (-. (ps -> ph) \/ -. (ph -> ps)))
31	29, 30, 8	3imtr4i 236	. . . . . 6 |- (-. ((ps -> ph) /\ (ph -> ps)) -> (-. ps <-> ph))
32	16, 31	sylbi 216	. . . . 5 |- (-. (ps <-> ph) -> (-. ps <-> ph))
33	17, 32	impbii 174	. . . 4 |- ((-. ps <-> ph) <-> -. (ps <-> ph))
34	2, 33	bitri 190	. . 3 |- ((ph <-> -. ps) <-> -. (ps <-> ph))
35	34	con2bii 238	. 2 |- ((ps <-> ph) <-> -. (ph <-> -. ps))
36	1, 35	bitri 190	1 |- ((ph <-> ps) <-> -. (ph <-> -. ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240

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 164  df-or 241  df-an 242

Copyright terms: Public domain