3impd Show Code edit
# Importation deduction for triple conjunction.
thm (3impd () (3imp1.1 (-> ph (-> ps (-> ch (-> th ta))))) (-> ph (-> (/\/\ ps ch th) ta)) 3imp1.1 com4l 3imp com12)
(-> ph (-> (/\/\ ps ch th) ta))
edit