Theorem e12 31760

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 31625	. 2 |- (. ph ,. ch ->. ps ).
3		e12.2	. 2 |- (. ph ,. ch ->. th ).
4		e12.3	. 2 |- ( ps -> ( th -> ta ) )
5	2, 3, 4	e22 31696	1 |- (. ph ,. ch ->. ta ).

Syntax hints:   -> wi 4   (.wvd1 31585   (.wvd2 31593

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 31586  df-vd2 31594

This theorem is referenced by:  e12an  31761  trsspwALT  31855  sspwtr  31858  pwtrVD  31863  snssiALTVD  31866  elex2VD  31877  elex22VD  31878  eqsbc3rVD  31879  en3lplem1VD  31882  3ornot23VD  31886  orbi1rVD  31887  19.21a3con13vVD  31891  exbirVD  31892  tratrbVD  31900  ssralv2VD  31905  sbcim2gVD  31914  sbcbiVD  31915  relopabVD  31940  19.41rgVD  31941  ax6e2eqVD  31946  ax6e2ndeqVD  31948  vk15.4jVD  31953  con3ALTVD  31955