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