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

Theorem e12 28179
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 28044 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 28115 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28003   (.wvd2 28012
This theorem is referenced by:  e12an  28180  trsspwALT  28274  sspwtr  28277  pwtrVD  28280  snssiALTVD  28282  elex2VD  28293  elex22VD  28294  eqsbc3rVD  28295  en3lplem1VD  28298  3ornot23VD  28302  orbi1rVD  28303  19.21a3con13vVD  28307  exbirVD  28308  tratrbVD  28316  ssralv2VD  28321  sbcim2gVD  28330  sbcbiVD  28331  relopabVD  28356  19.41rgVD  28357  a9e2eqVD  28362  a9e2ndeqVD  28364  vk15.4jVD  28369  con3ALTVD  28371
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 28004  df-vd2 28013
  Copyright terms: Public domain W3C validator