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

Theorem e2 28633
Description: A virtual deduction elimination rule. syl6 31 is e2 28633 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e2.1  |-  (. ph ,. ps  ->.  ch ).
e2.2  |-  ( ch 
->  th )
Assertion
Ref Expression
e2  |-  (. ph ,. ps  ->.  th ).

Proof of Theorem e2
StepHypRef Expression
1 e2.1 . . . 4  |-  (. ph ,. ps  ->.  ch ).
21dfvd2i 28578 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 31 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28579 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28570
This theorem is referenced by:  e2bi  28634  e2bir  28635  sspwtr  28835  pwtrVD  28838  pwtrrVD  28839  suctrALT2VD  28849  tpid3gVD  28855  en3lplem1VD  28856  3ornot23VD  28860  orbi1rVD  28861  19.21a3con13vVD  28865  tratrbVD  28874  syl5impVD  28876  ssralv2VD  28879  truniALTVD  28891  trintALTVD  28893  onfrALTlem3VD  28900  onfrALTlem2VD  28902  onfrALTlem1VD  28903  relopabVD  28914  19.41rgVD  28915  hbimpgVD  28917  a9e2eqVD  28920  a9e2ndeqVD  28922  sb5ALTVD  28926  vk15.4jVD  28927  con3ALTVD  28929
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-vd2 28571
  Copyright terms: Public domain W3C validator