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