Theorem e10 36715

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

Syntax hints:   -> wi 4   (.wvd1 36581

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 188  df-vd1 36582

This theorem is referenced by:  e10an  36716  en3lpVD  36885  3orbi123VD  36890  sbc3orgVD  36891  exbiriVD  36894  3impexpVD  36896  3impexpbicomVD  36897  al2imVD  36903  equncomVD  36909  trsbcVD  36918  sbcssgVD  36924  csbingVD  36925  onfrALTVD  36932  csbsngVD  36934  csbxpgVD  36935  csbresgVD  36936  csbrngVD  36937  csbima12gALTVD  36938  csbunigVD  36939  csbfv12gALTVD  36940  con5VD  36941  hbimpgVD  36945  hbalgVD  36946  hbexgVD  36947  ax6e2eqVD  36948  ax6e2ndeqVD  36950  e2ebindVD  36953  sb5ALTVD  36954