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

Theorem e2 28137
Description: A virtual deduction elimination rule. syl6 29 is e2 28137 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 28082 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 29 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28083 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28074
This theorem is referenced by:  e2bi  28138  e2bir  28139  sspwtr  28340  pwtrVD  28343  pwtrrVD  28345  suctrALT2VD  28357  tpid3gVD  28363  en3lplem1VD  28364  3ornot23VD  28368  orbi1rVD  28369  19.21a3con13vVD  28373  tratrbVD  28382  syl5impVD  28384  ssralv2VD  28387  truniALTVD  28399  trintALTVD  28401  onfrALTlem3VD  28408  onfrALTlem2VD  28410  onfrALTlem1VD  28411  relopabVD  28422  19.41rgVD  28423  hbimpgVD  28425  a9e2eqVD  28428  a9e2ndeqVD  28430  sb5ALTVD  28434  vk15.4jVD  28435  con3ALTVD  28437
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-vd2 28075
  Copyright terms: Public domain W3C validator