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

Theorem e12 32476
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 32341 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 32412 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 32301   (.wvd2 32309
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 371  df-vd1 32302  df-vd2 32310
This theorem is referenced by:  e12an  32477  trsspwALT  32571  sspwtr  32574  pwtrVD  32579  snssiALTVD  32582  elex2VD  32593  elex22VD  32594  eqsbc3rVD  32595  en3lplem1VD  32598  3ornot23VD  32602  orbi1rVD  32603  19.21a3con13vVD  32607  exbirVD  32608  tratrbVD  32616  ssralv2VD  32621  sbcim2gVD  32630  sbcbiVD  32631  relopabVD  32656  19.41rgVD  32657  ax6e2eqVD  32662  ax6e2ndeqVD  32664  vk15.4jVD  32669  con3ALTVD  32671
  Copyright terms: Public domain W3C validator