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