Theorem e11 33617

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

Hypotheses

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

Assertion

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

Proof of Theorem e11

Step	Hyp	Ref	Expression
1		e11.1	. 2 |- (. ph ->. ps ).
2		e11.2	. 2 |- (. ph ->. ch ).
3		e11.3	. . 3 |- ( ps -> ( ch -> th ) )
4	3	a1i 11	. 2 |- ( ps -> ( ps -> ( ch -> th ) ) )
5	1, 1, 2, 4	e111 33603	1 |- (. ph ->. th ).

Syntax hints:   -> wi 4   (.wvd1 33489

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 33490

This theorem is referenced by:  e11an  33618  e01  33620  e10  33623  elex2VD  33781  elex22VD  33782  eqsbc3rVD  33783  tpid3gVD  33785  3ornot23VD  33790  orbi1rVD  33791  3orbi123VD  33793  sbc3orgVD  33794  sbcoreleleqVD  33802  ordelordALTVD  33810  sbcim2gVD  33818  trsbcVD  33820  undif3VD  33825  sbcssgVD  33826  csbingVD  33827  onfrALTVD  33834  csbeq2gVD  33835  csbsngVD  33836  csbxpgVD  33837  csbresgVD  33838  csbrngVD  33839  csbima12gALTVD  33840  csbunigVD  33841  csbfv12gALTVD  33842  19.41rgVD  33845  2pm13.193VD  33846  hbimpgVD  33847  ax6e2eqVD  33850  2uasbanhVD  33854  notnot2ALTVD  33858