3imp1 Show Code edit
# Importation to left triple conjunction.
thm (3imp1 () (3imp1.1 (-> ph (-> ps (-> ch (-> th ta))))) (-> (/\ (/\/\ ph ps ch) th) ta) 3imp1.1 3imp imp)
(-> (/\ (/\/\ ph ps ch) th) ta)
edit