3simpc Show Code edit
# Simplification of triple conjunction.
thm (3simpc () () (-> (/\/\ ph ps ch) (/\ ps ch)) ph ps ch 3anrot ps ch ph 3simpa sylbi)
(-> (/\/\ ph ps ch) (/\ ps ch))
edit