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