xor Show Code edit
# Two ways to express "exclusive or." Theorem *5.22 of [bib/WhiteheadRussell]
# p. 124.
## Two ways to express Exclusive Or
thm (xor () () (<-> (-. (<-> ph ps)) (\/ (/\ ph (-. ps)) (/\ ps (-. ph)))) (-. ph) ps dfbi3 ph ps nbbn ps (-. ph) ancom ph notnot (-. ps) anbi1i orbi12i (/\ ps (-. ph)) (/\ ph (-. ps)) orcom bitr3i 3bitr3i)
(<-> (-. (<-> ph ps)) (\/ (/\ ph (-. ps)) (/\ ps (-. ph))))
edit