Theorem e12 33915

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

Syntax hints:   -> wi 4   (.wvd1 33740   (.wvd2 33748

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 369  df-vd1 33741  df-vd2 33749

This theorem is referenced by:  e12an  33916  trsspwALT  34010  sspwtr  34013  pwtrVD  34024  snssiALTVD  34027  elex2VD  34038  elex22VD  34039  eqsbc3rVD  34040  en3lplem1VD  34043  3ornot23VD  34047  orbi1rVD  34048  19.21a3con13vVD  34052  exbirVD  34053  tratrbVD  34062  ssralv2VD  34067  sbcim2gVD  34076  sbcbiVD  34077  relopabVD  34102  19.41rgVD  34103  ax6e2eqVD  34108  ax6e2ndeqVD  34110  vk15.4jVD  34115  con3ALTVD  34117