Theorem pm5.18 719

Description: Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive-or." (The proof was shortened by Andrew Salmon, 20-Jun-2011.)

Assertion

Ref	Expression
pm5.18	|- ((ph <-> ps) <-> -. (ph <-> -. ps))

Proof of Theorem pm5.18

Step	Hyp	Ref	Expression
1		pm2.65 148	. . . . . . . . 9 |- ((ps -> ph) -> ((ps -> -. ph) -> -. ps))
2		con2 105	. . . . . . . . 9 |- ((ph -> -. ps) -> (ps -> -. ph))
3	1, 2	syl5com 63	. . . . . . . 8 |- ((ph -> -. ps) -> ((ps -> ph) -> -. ps))
4		pm2.65 148	. . . . . . . . 9 |- ((ph -> ps) -> ((ph -> -. ps) -> -. ph))
5	4	com12 14	. . . . . . . 8 |- ((ph -> -. ps) -> ((ph -> ps) -> -. ph))
6	3, 5	anim12d 614	. . . . . . 7 |- ((ph -> -. ps) -> (((ps -> ph) /\ (ph -> ps)) -> (-. ps /\ -. ph)))
7	6	com12 14	. . . . . 6 |- (((ps -> ph) /\ (ph -> ps)) -> ((ph -> -. ps) -> (-. ps /\ -. ph)))
8	7	ancoms 482	. . . . 5 |- (((ph -> ps) /\ (ps -> ph)) -> ((ph -> -. ps) -> (-. ps /\ -. ph)))
9		pm4.65 257	. . . . 5 |- (-. (-. ps -> ph) <-> (-. ps /\ -. ph))
10	8, 9	syl6ibr 229	. . . 4 |- (((ph -> ps) /\ (ps -> ph)) -> ((ph -> -. ps) -> -. (-. ps -> ph)))
11		df-an 241	. . . . . 6 |- ((ph /\ ps) <-> -. (ph -> -. ps))
12		ax-1 4	. . . . . . . 8 |- (ps -> (ph -> ps))
13		ax-1 4	. . . . . . . 8 |- (ph -> (ps -> ph))
14	12, 13	anim12i 358	. . . . . . 7 |- ((ps /\ ph) -> ((ph -> ps) /\ (ps -> ph)))
15	14	ancoms 482	. . . . . 6 |- ((ph /\ ps) -> ((ph -> ps) /\ (ps -> ph)))
16	11, 15	sylbir 217	. . . . 5 |- (-. (ph -> -. ps) -> ((ph -> ps) /\ (ps -> ph)))
17		pm2.21 91	. . . . . . . 8 |- (-. ph -> (ph -> ps))
18		pm2.21 91	. . . . . . . 8 |- (-. ps -> (ps -> ph))
19	17, 18	anim12i 358	. . . . . . 7 |- ((-. ph /\ -. ps) -> ((ph -> ps) /\ (ps -> ph)))
20	19	ancoms 482	. . . . . 6 |- ((-. ps /\ -. ph) -> ((ph -> ps) /\ (ps -> ph)))
21	9, 20	sylbi 215	. . . . 5 |- (-. (-. ps -> ph) -> ((ph -> ps) /\ (ps -> ph)))
22	16, 21	ja 151	. . . 4 |- (((ph -> -. ps) -> -. (-. ps -> ph)) -> ((ph -> ps) /\ (ps -> ph)))
23	10, 22	impbii 173	. . 3 |- (((ph -> ps) /\ (ps -> ph)) <-> ((ph -> -. ps) -> -. (-. ps -> ph)))
24		notnot 177	. . 3 |- (((ph -> -. ps) -> -. (-. ps -> ph)) <-> -. -. ((ph -> -. ps) -> -. (-. ps -> ph)))
25	23, 24	bitri 189	. 2 |- (((ph -> ps) /\ (ps -> ph)) <-> -. -. ((ph -> -. ps) -> -. (-. ps -> ph)))
26		dfbi2 569	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
27		dfbi1 174	. . 3 |- ((ph <-> -. ps) <-> -. ((ph -> -. ps) -> -. (-. ps -> ph)))
28	27	notbii 203	. 2 |- (-. (ph <-> -. ps) <-> -. -. ((ph -> -. ps) -> -. (-. ps -> ph)))
29	25, 26, 28	3bitr4i 199	1 |- ((ph <-> ps) <-> -. (ph <-> -. ps))

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

This theorem is referenced by:  nbbn 721  pm5.15 726  pm5.16 727  pm5.19 729  dfbi3 730  xor3 734  assxor 14009

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 163  df-an 241

Copyright terms: Public domain