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

Theorem e2 28403
Description: A virtual deduction elimination rule. syl6 29 is e2 28403 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 28354 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 29 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 28355 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28346
This theorem is referenced by:  e2bi  28404  e2bir  28405  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  suctrALT2VD  28612  tpid3gVD  28618  en3lplem1VD  28619  3ornot23VD  28623  orbi1rVD  28624  19.21a3con13vVD  28628  tratrbVD  28637  syl5impVD  28639  ssralv2VD  28642  truniALTVD  28654  trintALTVD  28656  onfrALTlem3VD  28663  onfrALTlem2VD  28665  onfrALTlem1VD  28666  relopabVD  28677  19.41rgVD  28678  hbimpgVD  28680  a9e2eqVD  28683  a9e2ndeqVD  28685  sb5ALTVD  28689  vk15.4jVD  28690  con3ALTVD  28692
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 28347
  Copyright terms: Public domain W3C validator