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

Theorem e2 28708
Description: A virtual deduction elimination rule. syl6 29 is e2 28708 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 28653 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 29 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28654 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28645
This theorem is referenced by:  e2bi  28709  e2bir  28710  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  suctrALT2VD  28928  tpid3gVD  28934  en3lplem1VD  28935  3ornot23VD  28939  orbi1rVD  28940  19.21a3con13vVD  28944  tratrbVD  28953  syl5impVD  28955  ssralv2VD  28958  truniALTVD  28970  trintALTVD  28972  onfrALTlem3VD  28979  onfrALTlem2VD  28981  onfrALTlem1VD  28982  relopabVD  28993  19.41rgVD  28994  hbimpgVD  28996  a9e2eqVD  28999  a9e2ndeqVD  29001  sb5ALTVD  29005  vk15.4jVD  29006  con3ALTVD  29008
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 28646
  Copyright terms: Public domain W3C validator