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

Theorem e2 37078
Description: A virtual deduction elimination rule. syl6 33 is e2 37078 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 37023 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 33 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 37024 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 37015
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 190  df-an 378  df-vd2 37016
This theorem is referenced by:  e2bi  37079  e2bir  37080  sspwtr  37272  pwtrVD  37283  pwtrrVD  37284  suctrALT2VD  37295  tpid3gVD  37301  en3lplem1VD  37302  3ornot23VD  37306  orbi1rVD  37307  19.21a3con13vVD  37311  tratrbVD  37321  syl5impVD  37323  ssralv2VD  37326  truniALTVD  37338  trintALTVD  37340  onfrALTlem3VD  37347  onfrALTlem2VD  37349  onfrALTlem1VD  37350  relopabVD  37361  19.41rgVD  37362  hbimpgVD  37364  ax6e2eqVD  37367  ax6e2ndeqVD  37369  sb5ALTVD  37373  vk15.4jVD  37374  con3ALTVD  37376
  Copyright terms: Public domain W3C validator