3impdi Show Code edit
# Importation inference (undistribute conjunction).
thm (3impdi () (3impdi.1 (-> (/\ (/\ ph ps) (/\ ph ch)) th)) (-> (/\/\ ph ps ch) th) 3impdi.1 anandis 3impb)
(-> (/\/\ ph ps ch) th)
edit