pm5.63 Show Code edit
# Theorem *5.63 of [bib/WhiteheadRussell] p. 125.
thm (pm5.63 () () (<-> (\/ ph ps) (\/ ph (/\ (-. ph) ps))) ph ps pm2.53 ancld orrd ph ps pm2.24 (-. ph) ps pm3.4 jaoi orrd impbii)
(<-> (\/ ph ps) (\/ ph (/\ (-. ph) ps)))
edit