pm5.24 Show Code edit
# Theorem *5.24 of [bib/WhiteheadRussell] p. 124.
## Two ways to express Exclusive Or
thm (pm5.24 () () (<-> (-. (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) (\/ (/\ ph (-. ps)) (/\ ps (-. ph)))) ph ps dfbi3 notbii ph ps xor bitr3i)
(<-> (-. (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) (\/ (/\ ph (-. ps)) (/\ ps (-. ph))))
edit