Theorem e10 38919

Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e10.1	|- (. ph ->. ps ).
e10.2	|- ch
e10.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
e10	|- (. ph ->. th ).

Proof of Theorem e10

Step	Hyp	Ref	Expression
1		e10.1	. 2 |- (. ph ->. ps ).
2		e10.2	. . 3 |- ch
3	2	vd01 38822	. 2 |- (. ph ->. ch ).
4		e10.3	. 2 |- ( ps -> ( ch -> th ) )
5	1, 3, 4	e11 38913	1 |- (. ph ->. th ).

Syntax hints:   -> wi 4   (.wvd1 38785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-vd1 38786

This theorem is referenced by:  e10an  38920  en3lpVD  39080  3orbi123VD  39085  sbc3orgVD  39086  exbiriVD  39089  3impexpVD  39091  3impexpbicomVD  39092  al2imVD  39098  equncomVD  39104  trsbcVD  39113  sbcssgVD  39119  csbingVD  39120  onfrALTVD  39127  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  con5VD  39136  hbimpgVD  39140  hbalgVD  39141  hbexgVD  39142  ax6e2eqVD  39143  ax6e2ndeqVD  39145  e2ebindVD  39148  sb5ALTVD  39149