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

Theorem e12 31760
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 31625 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 31696 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 31585   (.wvd2 31593
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 31586  df-vd2 31594
This theorem is referenced by:  e12an  31761  trsspwALT  31855  sspwtr  31858  pwtrVD  31863  snssiALTVD  31866  elex2VD  31877  elex22VD  31878  eqsbc3rVD  31879  en3lplem1VD  31882  3ornot23VD  31886  orbi1rVD  31887  19.21a3con13vVD  31891  exbirVD  31892  tratrbVD  31900  ssralv2VD  31905  sbcim2gVD  31914  sbcbiVD  31915  relopabVD  31940  19.41rgVD  31941  ax6e2eqVD  31946  ax6e2ndeqVD  31948  vk15.4jVD  31953  con3ALTVD  31955
  Copyright terms: Public domain W3C validator