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

Theorem e2 28806
Description: A virtual deduction elimination rule. syl6 32 is e2 28806 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 28751 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 32 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28752 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28743
This theorem is referenced by:  e2bi  28807  e2bir  28808  sspwtr  29008  pwtrVD  29011  pwtrrVD  29012  suctrALT2VD  29022  tpid3gVD  29028  en3lplem1VD  29029  3ornot23VD  29033  orbi1rVD  29034  19.21a3con13vVD  29038  tratrbVD  29047  syl5impVD  29049  ssralv2VD  29052  truniALTVD  29064  trintALTVD  29066  onfrALTlem3VD  29073  onfrALTlem2VD  29075  onfrALTlem1VD  29076  relopabVD  29087  19.41rgVD  29088  hbimpgVD  29090  a9e2eqVD  29093  a9e2ndeqVD  29095  sb5ALTVD  29099  vk15.4jVD  29100  con3ALTVD  29102
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 179  df-an 362  df-vd2 28744
  Copyright terms: Public domain W3C validator