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

Theorem e2 36924
Description: A virtual deduction elimination rule. syl6 34 is e2 36924 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 36869 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 34 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 36870 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 36861
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 188  df-an 372  df-vd2 36862
This theorem is referenced by:  e2bi  36925  e2bir  36926  sspwtr  37125  pwtrVD  37136  pwtrrVD  37137  suctrALT2VD  37148  tpid3gVD  37154  en3lplem1VD  37155  3ornot23VD  37159  orbi1rVD  37160  19.21a3con13vVD  37164  tratrbVD  37174  syl5impVD  37176  ssralv2VD  37179  truniALTVD  37191  trintALTVD  37193  onfrALTlem3VD  37200  onfrALTlem2VD  37202  onfrALTlem1VD  37203  relopabVD  37214  19.41rgVD  37215  hbimpgVD  37217  ax6e2eqVD  37220  ax6e2ndeqVD  37222  sb5ALTVD  37226  vk15.4jVD  37227  con3ALTVD  37229
  Copyright terms: Public domain W3C validator