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