ancr Show Code edit
## Add antecedent
thm (ancr () () (-> (-> ph ps) (-> ph (/\ ps ph))) ph ps pm3.21 a2i)
(-> (-> ph ps) (-> ph (/\ ps ph)))
edit