3simpr1 Show Code edit
# Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
thm (3simpr1 () () (-> (/\ ph (/\/\ ps ch th)) ps) ps ch th 3simp1 ph adantl)
(-> (/\ ph (/\/\ ps ch th)) ps)
edit