dn1 Show Code edit
# A single axiom for Boolean algebra known as DN_1. See
# [[http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf]].
# (Contributed by Jeffrey Hankins, 3-Jul-2009.)
thm (dn1 () () (<-> (-. (\/ (-. (\/ (-. (\/ ph ps)) ch)) (-. (\/ ph (-. (\/ (-. ch) (-. (\/ ch th)))))))) ch) (\/ (-. (\/ ph ps)) ch) (\/ ph (-. (\/ (-. ch) (-. (\/ ch th))))) anor ph ps ioran ph (-> (-. ps) ch) pm2.24 com23 ch (\/ ch th) anor ch (-. ph) ax-1 (-. ps) a1d (\/ ch th) adantr sylbir jaoi com13 imp sylbi ch (\/ ph (-. (\/ (-. ch) (-. (\/ ch th))))) ax-1 jaoi imp ch (-. (\/ ph ps)) olc ch ph pm2.24 ch (-> (-. th) ph) pm2.24 imp3a ch th ioran syl5ib jaod con3d orrd jca impbii bitr3i)
(<-> (-. (\/ (-. (\/ (-. (\/ ph ps)) ch)) (-. (\/ ph (-. (\/ (-. ch) (-. (\/ ch th)))))))) ch)
edit