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

Theorem e2 28441
Description: A virtual deduction elimination rule. syl6 31 is e2 28441 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 28386 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 31 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28387 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28378
This theorem is referenced by:  e2bi  28442  e2bir  28443  sspwtr  28643  pwtrVD  28646  pwtrrVD  28647  suctrALT2VD  28657  tpid3gVD  28663  en3lplem1VD  28664  3ornot23VD  28668  orbi1rVD  28669  19.21a3con13vVD  28673  tratrbVD  28682  syl5impVD  28684  ssralv2VD  28687  truniALTVD  28699  trintALTVD  28701  onfrALTlem3VD  28708  onfrALTlem2VD  28710  onfrALTlem1VD  28711  relopabVD  28722  19.41rgVD  28723  hbimpgVD  28725  a9e2eqVD  28728  a9e2ndeqVD  28730  sb5ALTVD  28734  vk15.4jVD  28735  con3ALTVD  28737
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 28379
  Copyright terms: Public domain W3C validator