Theorem e11 36704

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 36690	1 |- (. ph ->. th ).

Syntax hints:   -> wi 4   (.wvd1 36576

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 36577

This theorem is referenced by:  e11an  36705  e01  36707  e10  36710  elex2VD  36873  elex22VD  36874  eqsbc3rVD  36875  tpid3gVD  36877  3ornot23VD  36882  orbi1rVD  36883  3orbi123VD  36885  sbc3orgVD  36886  sbcoreleleqVD  36895  ordelordALTVD  36903  sbcim2gVD  36911  trsbcVD  36913  undif3VD  36918  sbcssgVD  36919  csbingVD  36920  onfrALTVD  36927  csbeq2gVD  36928  csbsngVD  36929  csbxpgVD  36930  csbresgVD  36931  csbrngVD  36932  csbima12gALTVD  36933  csbunigVD  36934  csbfv12gALTVD  36935  19.41rgVD  36938  2pm13.193VD  36939  hbimpgVD  36940  ax6e2eqVD  36943  2uasbanhVD  36947  notnot2ALTVD  36951