idd Show Code edit
## Identity Deduction
##
## Identity written as an deduction.
##
thm (idd () () (-> ph (-> ps ps)) ps id ph a1i)
(-> ph (-> ps ps))
edit