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

Theorem e2 33811
Description: A virtual deduction elimination rule. syl6 33 is e2 33811 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 33756 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 e2.2 . . 3  |-  ( ch 
->  th )
42, 3syl6 33 . 2  |-  ( ph  ->  ( ps  ->  th )
)
54dfvd2ir 33757 1  |-  (. ph ,. ps  ->.  th ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd2 33748
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 369  df-vd2 33749
This theorem is referenced by:  e2bi  33812  e2bir  33813  sspwtr  34013  pwtrVD  34024  pwtrrVD  34025  suctrALT2VD  34036  tpid3gVD  34042  en3lplem1VD  34043  3ornot23VD  34047  orbi1rVD  34048  19.21a3con13vVD  34052  tratrbVD  34062  syl5impVD  34064  ssralv2VD  34067  truniALTVD  34079  trintALTVD  34081  onfrALTlem3VD  34088  onfrALTlem2VD  34090  onfrALTlem1VD  34091  relopabVD  34102  19.41rgVD  34103  hbimpgVD  34105  ax6e2eqVD  34108  ax6e2ndeqVD  34110  sb5ALTVD  34114  vk15.4jVD  34115  con3ALTVD  34117
  Copyright terms: Public domain W3C validator