ancri Show Code edit
# Deduction conjoining antecedent to right of consequent.
## Add Antecedent
##
## (-> ph [ ps ] )
## (-> ph (/\ [ ps ] ph))
##
thm (ancri () (ancri.1 (-> ph ps)) (-> ph (/\ ps ph)) ancri.1 ph id jca)
(-> ph (/\ ps ph))
edit