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

Theorem e2 28075
Description: A virtual deduction elimination rule. syl6 31 is e2 28075 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 28020 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 31 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28021 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28012
This theorem is referenced by:  e2bi  28076  e2bir  28077  sspwtr  28277  pwtrVD  28280  pwtrrVD  28281  suctrALT2VD  28291  tpid3gVD  28297  en3lplem1VD  28298  3ornot23VD  28302  orbi1rVD  28303  19.21a3con13vVD  28307  tratrbVD  28316  syl5impVD  28318  ssralv2VD  28321  truniALTVD  28333  trintALTVD  28335  onfrALTlem3VD  28342  onfrALTlem2VD  28344  onfrALTlem1VD  28345  relopabVD  28356  19.41rgVD  28357  hbimpgVD  28359  a9e2eqVD  28362  a9e2ndeqVD  28364  sb5ALTVD  28368  vk15.4jVD  28369  con3ALTVD  28371
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 28013
  Copyright terms: Public domain W3C validator