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

Theorem e12 28773
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 28638 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 28709 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28597   (.wvd2 28606
This theorem is referenced by:  e12an  28774  trsspwALT  28868  sspwtr  28871  pwtrVD  28874  snssiALTVD  28876  elex2VD  28887  elex22VD  28888  eqsbc3rVD  28889  en3lplem1VD  28892  3ornot23VD  28896  orbi1rVD  28897  19.21a3con13vVD  28901  exbirVD  28902  tratrbVD  28910  ssralv2VD  28915  sbcim2gVD  28924  sbcbiVD  28925  relopabVD  28950  19.41rgVD  28951  a9e2eqVD  28956  a9e2ndeqVD  28958  vk15.4jVD  28963  con3ALTVD  28965
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 178  df-an 361  df-vd1 28598  df-vd2 28607
  Copyright terms: Public domain W3C validator