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

Theorem e12 28813
Description: A virtual deduction elimination rule. (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 28677 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 28748 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636   (.wvd2 28645
This theorem is referenced by:  e12an  28814  trsspwALT  28908  sspwtr  28911  pwtrVD  28914  snssiALTVD  28918  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  en3lplem1VD  28935  3ornot23VD  28939  orbi1rVD  28940  19.21a3con13vVD  28944  exbirVD  28945  tratrbVD  28953  ssralv2VD  28958  sbcim2gVD  28967  sbcbiVD  28968  relopabVD  28993  19.41rgVD  28994  a9e2eqVD  28999  a9e2ndeqVD  29001  vk15.4jVD  29006  con3ALTVD  29008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-vd1 28637  df-vd2 28646
  Copyright terms: Public domain W3C validator