Theorem e11 38913

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 38899	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:  e11an  38914  e01  38916  e10  38919  elex2VD  39073  elex22VD  39074  eqsbc3rVD  39075  tpid3gVD  39077  3ornot23VD  39082  orbi1rVD  39083  3orbi123VD  39085  sbc3orgVD  39086  sbcoreleleqVD  39095  ordelordALTVD  39103  sbcim2gVD  39111  trsbcVD  39113  undif3VD  39118  sbcssgVD  39119  csbingVD  39120  onfrALTVD  39127  csbeq2gVD  39128  csbsngVD  39129  csbxpgVD  39130  csbresgVD  39131  csbrngVD  39132  csbima12gALTVD  39133  csbunigVD  39134  csbfv12gALTVD  39135  19.41rgVD  39138  2pm13.193VD  39139  hbimpgVD  39140  ax6e2eqVD  39143  2uasbanhVD  39147  notnotrALTVD  39151