pm5.71 Show Code edit
# Theorem *5.71 of [bib/WhiteheadRussell] p. 125. (Contributed by Roy F.
# Longton, 23-Jun-2005.)
thm (pm5.71 () () (-> (-> ps (-. ch)) (<-> (/\ (\/ ph ps) ch) (/\ ph ch))) ps ph orel2 ph ps orc impbid1 ch anbi1d ch (<-> (\/ ph ps) ph) pm2.21 pm5.32rd ja)
(-> (-> ps (-. ch)) (<-> (/\ (\/ ph ps) ch) (/\ ph ch)))
edit