Theorem e12 37107

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

Syntax hints:   -> wi 4   (.wvd1 36938   (.wvd2 36946

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 190  df-an 377  df-vd1 36939  df-vd2 36947

This theorem is referenced by:  e12an  37108  trsspwALT  37202  sspwtr  37205  pwtrVD  37216  snssiALTVD  37219  elex2VD  37230  elex22VD  37231  eqsbc3rVD  37232  en3lplem1VD  37235  3ornot23VD  37239  orbi1rVD  37240  19.21a3con13vVD  37244  exbirVD  37245  tratrbVD  37254  ssralv2VD  37259  sbcim2gVD  37268  sbcbiVD  37269  relopabVD  37294  19.41rgVD  37295  ax6e2eqVD  37300  ax6e2ndeqVD  37302  vk15.4jVD  37307  con3ALTVD  37309