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

Theorem e2 31686
Description: A virtual deduction elimination rule. syl6 33 is e2 31686 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 31631 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 33 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 31632 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 31623
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 185  df-an 371  df-vd2 31624
This theorem is referenced by:  e2bi  31687  e2bir  31688  sspwtr  31888  pwtrVD  31893  pwtrrVD  31894  suctrALT2VD  31905  tpid3gVD  31911  en3lplem1VD  31912  3ornot23VD  31916  orbi1rVD  31917  19.21a3con13vVD  31921  tratrbVD  31930  syl5impVD  31932  ssralv2VD  31935  truniALTVD  31947  trintALTVD  31949  onfrALTlem3VD  31956  onfrALTlem2VD  31958  onfrALTlem1VD  31959  relopabVD  31970  19.41rgVD  31971  hbimpgVD  31973  ax6e2eqVD  31976  ax6e2ndeqVD  31978  sb5ALTVD  31982  vk15.4jVD  31983  con3ALTVD  31985
  Copyright terms: Public domain W3C validator