Theorem e12 32476

Description: A virtual deduction elimination rule (see sylsyld 56). (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 32341	. 2 |- (. ph ,. ch ->. ps ).
3		e12.2	. 2 |- (. ph ,. ch ->. th ).
4		e12.3	. 2 |- ( ps -> ( th -> ta ) )
5	2, 3, 4	e22 32412	1 |- (. ph ,. ch ->. ta ).

Syntax hints:   -> wi 4   (.wvd1 32301   (.wvd2 32309

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-an 371  df-vd1 32302  df-vd2 32310

This theorem is referenced by:  e12an  32477  trsspwALT  32571  sspwtr  32574  pwtrVD  32579  snssiALTVD  32582  elex2VD  32593  elex22VD  32594  eqsbc3rVD  32595  en3lplem1VD  32598  3ornot23VD  32602  orbi1rVD  32603  19.21a3con13vVD  32607  exbirVD  32608  tratrbVD  32616  ssralv2VD  32621  sbcim2gVD  32630  sbcbiVD  32631  relopabVD  32656  19.41rgVD  32657  ax6e2eqVD  32662  ax6e2ndeqVD  32664  vk15.4jVD  32669  con3ALTVD  32671