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

Theorem e1_ 28704
Description: A Virtual deduction elimination rule. syl 15 is e1_ 28704 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 28638 . . 3  |-  ( ph  ->  ps )
3 e1_.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 15 . 2  |-  ( ph  ->  ch )
54dfvd1ir 28640 1  |-  (. ph  ->.  ch
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636
This theorem is referenced by:  e1bi  28706  e1bir  28707  snelpwrVD  28922  unipwrVD  28924  sstrALT2VD  28926  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  zfregs2VD  28933  tpid3gVD  28934  en3lplem1VD  28935  en3lpVD  28937  3ornot23VD  28939  3orbi123VD  28942  sbc3orgVD  28943  exbirVD  28945  3impexpVD  28948  3impexpbicomVD  28949  sbcoreleleqVD  28951  tratrbVD  28953  3ax5VD  28954  syl5impVD  28955  ssralv2VD  28958  ordelordALTVD  28959  sbcim2gVD  28967  trsbcVD  28969  truniALTVD  28970  trintALTVD  28972  undif3VD  28974  sbcssVD  28975  csbingVD  28976  onfrALTlem3VD  28979  simplbi2comgVD  28980  onfrALTlem2VD  28981  onfrALTVD  28983  csbeq2gVD  28984  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  con5VD  28992  relopabVD  28993  19.41rgVD  28994  2pm13.193VD  28995  hbimpgVD  28996  hbalgVD  28997  hbexgVD  28998  a9e2eqVD  28999  a9e2ndVD  29000  a9e2ndeqVD  29001  2sb5ndVD  29002  2uasbanhVD  29003  e2ebindVD  29004  sb5ALTVD  29005  vk15.4jVD  29006  notnot2ALTVD  29007  con3ALTVD  29008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-vd1 28637
  Copyright terms: Public domain W3C validator