Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e12 Structured version   Unicode version

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
StepHypRef Expression
1 e12.1 . . 3  |-  (. ph  ->.  ps
).
21vd12 33780 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 33851 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator