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