pm5.18 Show Code edit
# Theorem *5.18 of [bib/WhiteheadRussell] p. 124. This theorem says that
# logical equivalence is the same as negated "exclusive-or."
## Logical Equivalence is Negated Exclusive Or
thm (pm5.18 () () (<-> (<-> ph ps) (-. (<-> ph (-. ps)))) ph ps bicom ph (-. ps) bicom ps ph pm2.61 ps ph pm2.65 ph ps con2 syl5 anim12d (-. ps) ph dfbi2 syl5ib ph ps annim syl6ib com12 (-> ps ph) (-> ph ps) imnan sylib ps ph dfbi2 notbii sylibr ps ph dfbi2 notbii ps ph pm2.5 ps ph annim ph (-. ps) pm2.21 ps adantl sylbir jca ph ps annim ph (-. ps) ax-1 (-. ps) adantr sylbir ph ps pm2.51 jca jaoi (-> ps ph) (-> ph ps) ianor (-. ps) ph dfbi2 3imtr4i sylbi impbii bitri con2bii bitri)
(<-> (<-> ph ps) (-. (<-> ph (-. ps))))