Theorem e12 38951

Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e12.1	|- (. ph ->. ps ).
e12.2	|- (. ph ,. ch ->. th ).
e12.3	|- ( ps -> ( th -> ta ) )

Assertion

Ref	Expression
e12	|- (. ph ,. ch ->. ta ).

Proof of Theorem e12

Step	Hyp	Ref	Expression
1		e12.1	. . 3 |- (. ph ->. ps ).
2	1	vd12 38825	. 2 |- (. ph ,. ch ->. ps ).
3		e12.2	. 2 |- (. ph ,. ch ->. th ).
4		e12.3	. 2 |- ( ps -> ( th -> ta ) )
5	2, 3, 4	e22 38896	1 |- (. ph ,. ch ->. ta ).

Syntax hints:   -> wi 4   (.wvd1 38785   (.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-vd1 38786  df-vd2 38794

This theorem is referenced by:  e12an  38952  trsspwALT  39045  sspwtr  39048  pwtrVD  39059  snssiALTVD  39062  elex2VD  39073  elex22VD  39074  eqsbc3rVD  39075  en3lplem1VD  39078  3ornot23VD  39082  orbi1rVD  39083  19.21a3con13vVD  39087  exbirVD  39088  tratrbVD  39097  ssralv2VD  39102  sbcim2gVD  39111  sbcbiVD  39112  relopabVD  39137  19.41rgVD  39138  ax6e2eqVD  39143  ax6e2ndeqVD  39145  vk15.4jVD  39150  con3ALTVD  39152