pm5.16 Show Code edit
# Theorem *5.16 of [bib/WhiteheadRussell] p. 124.
thm (pm5.16 () () (-. (/\ (<-> ph ps) (<-> ph (-. ps)))) ph ps pm5.18 biimpi (<-> ph ps) (<-> ph (-. ps)) pm4.62 mpbi (<-> ph ps) (<-> ph (-. ps)) ianor mpbir)
(-. (/\ (<-> ph ps) (<-> ph (-. ps))))
edit