Theorem e2 38856

Description: A virtual deduction elimination rule. syl6 35 is e2 38856 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e2.1	|- (. ph ,. ps ->. ch ).
e2.2	|- ( ch -> th )

Assertion

Ref	Expression
e2	|- (. ph ,. ps ->. th ).

Proof of Theorem e2

Step	Hyp	Ref	Expression
1		e2.1	. . . 4 |- (. ph ,. ps ->. ch ).
2	1	dfvd2i 38801	. . 3 |- ( ph -> ( ps -> ch ) )
3		e2.2	. . 3 |- ( ch -> th )
4	2, 3	syl6 35	. 2 |- ( ph -> ( ps -> th ) )
5	4	dfvd2ir 38802	1 |- (. ph ,. ps ->. th ).

Syntax hints:   -> wi 4   (.wvd2 38793

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-an 386  df-vd2 38794

This theorem is referenced by:  e2bi  38857  e2bir  38858  sspwtr  39048  pwtrVD  39059  pwtrrVD  39060  suctrALT2VD  39071  tpid3gVD  39077  en3lplem1VD  39078  3ornot23VD  39082  orbi1rVD  39083  19.21a3con13vVD  39087  tratrbVD  39097  syl5impVD  39099  ssralv2VD  39102  truniALTVD  39114  trintALTVD  39116  onfrALTlem3VD  39123  onfrALTlem2VD  39125  onfrALTlem1VD  39126  relopabVD  39137  19.41rgVD  39138  hbimpgVD  39140  ax6e2eqVD  39143  ax6e2ndeqVD  39145  sb5ALTVD  39149  vk15.4jVD  39150  con3ALTVD  39152