Theorem e10 33666

Description: A virtual deduction elimination rule (see mpisyl 18). (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 33569	. 2 |- (. ph ->. ch ).
4		e10.3	. 2 |- ( ps -> ( ch -> th ) )
5	1, 3, 4	e11 33660	1 |- (. ph ->. th ).

Syntax hints:   -> wi 4   (.wvd1 33532

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 185  df-vd1 33533

This theorem is referenced by:  e10an  33667  en3lpVD  33831  3orbi123VD  33836  sbc3orgVD  33837  exbiriVD  33840  3impexpVD  33842  3impexpbicomVD  33843  al2imVD  33848  equncomVD  33854  trsbcVD  33863  sbcssgVD  33869  csbingVD  33870  onfrALTVD  33877  csbsngVD  33879  csbxpgVD  33880  csbresgVD  33881  csbrngVD  33882  csbima12gALTVD  33883  csbunigVD  33884  csbfv12gALTVD  33885  con5VD  33886  hbimpgVD  33890  hbalgVD  33891  hbexgVD  33892  ax6e2eqVD  33893  ax6e2ndeqVD  33895  e2ebindVD  33898  sb5ALTVD  33899