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

Theorem e12 28499
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 28372 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 28443 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337   (.wvd2 28346
This theorem is referenced by:  e12an  28500  trsspwALT  28592  sspwtr  28595  pwtrVD  28598  snssiALTVD  28602  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  en3lplem1VD  28619  3ornot23VD  28623  orbi1rVD  28624  19.21a3con13vVD  28628  exbirVD  28629  tratrbVD  28637  ssralv2VD  28642  sbcim2gVD  28651  sbcbiVD  28652  relopabVD  28677  19.41rgVD  28678  a9e2eqVD  28683  a9e2ndeqVD  28685  vk15.4jVD  28690  con3ALTVD  28692
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 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator