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

Theorem e1_ 31051
Description: A Virtual deduction elimination rule. syl 16 is e1_ 31051 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e1_.1  |-  (. ph  ->.  ps
).
e1_.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
e1_  |-  (. ph  ->.  ch
).

Proof of Theorem e1_
StepHypRef Expression
1 e1_.1 . . . 4  |-  (. ph  ->.  ps
).
21in1 30985 . . 3  |-  ( ph  ->  ps )
3 e1_.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 16 . 2  |-  ( ph  ->  ch )
54dfvd1ir 30987 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 30983
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-vd1 30984
This theorem is referenced by:  e1bi  31053  e1bir  31054  snelpwrVD  31269  unipwrVD  31270  sstrALT2VD  31272  elex2VD  31276  elex22VD  31277  eqsbc3rVD  31278  zfregs2VD  31279  tpid3gVD  31280  en3lplem1VD  31281  en3lpVD  31283  3ornot23VD  31285  3orbi123VD  31288  sbc3orgVD  31289  exbirVD  31291  3impexpVD  31294  3impexpbicomVD  31295  sbcoreleleqVD  31297  tratrbVD  31299  3ax4VD  31300  syl5impVD  31301  ssralv2VD  31304  ordelordALTVD  31305  sbcim2gVD  31313  trsbcVD  31315  truniALTVD  31316  trintALTVD  31318  undif3VD  31320  sbcssgVD  31321  csbingVD  31322  onfrALTlem3VD  31325  simplbi2comgVD  31326  onfrALTlem2VD  31327  onfrALTVD  31329  csbeq2gVD  31330  csbsngVD  31331  csbxpgVD  31332  csbresgVD  31333  csbrngVD  31334  csbima12gALTVD  31335  csbunigVD  31336  csbfv12gALTVD  31337  con5VD  31338  relopabVD  31339  19.41rgVD  31340  2pm13.193VD  31341  hbimpgVD  31342  hbalgVD  31343  hbexgVD  31344  ax6e2eqVD  31345  ax6e2ndVD  31346  ax6e2ndeqVD  31347  2sb5ndVD  31348  2uasbanhVD  31349  e2ebindVD  31350  sb5ALTVD  31351  vk15.4jVD  31352  notnot2ALTVD  31353  con3ALTVD  31354
  Copyright terms: Public domain W3C validator