pm5.21ni Show Code edit
## Two propositions implying a false one are equivalent
thm (pm5.21ni () (pm5.21ni.1 (-> ph ps) pm5.21ni.2 (-> ch ps)) (-> (-. ps) (<-> ph ch)) ph ch pm5.21 pm5.21ni.1 con3i pm5.21ni.2 con3i sylanc)
(-> (-. ps) (<-> ph ch))
edit