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

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

Proof of Theorem e1a
StepHypRef Expression
1 e1a.1 . . . 4  |-  (. ph  ->.  ps
).
21in1 36627 . . 3  |-  ( ph  ->  ps )
3 e1a.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 17 . 2  |-  ( ph  ->  ch )
54dfvd1ir 36629 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36625
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-vd1 36626
This theorem is referenced by:  e1bi  36694  e1bir  36695  snelpwrVD  36915  unipwrVD  36916  sstrALT2VD  36918  elex2VD  36922  elex22VD  36923  eqsbc3rVD  36924  zfregs2VD  36925  tpid3gVD  36926  en3lplem1VD  36927  en3lpVD  36929  3ornot23VD  36931  3orbi123VD  36934  sbc3orgVD  36935  exbirVD  36937  3impexpVD  36940  3impexpbicomVD  36941  sbcoreleleqVD  36944  tratrbVD  36946  al2imVD  36947  syl5impVD  36948  ssralv2VD  36951  ordelordALTVD  36952  sbcim2gVD  36960  trsbcVD  36962  truniALTVD  36963  trintALTVD  36965  undif3VD  36967  sbcssgVD  36968  csbingVD  36969  onfrALTlem3VD  36972  simplbi2comtVD  36973  onfrALTlem2VD  36974  onfrALTVD  36976  csbeq2gVD  36977  csbsngVD  36978  csbxpgVD  36979  csbresgVD  36980  csbrngVD  36981  csbima12gALTVD  36982  csbunigVD  36983  csbfv12gALTVD  36984  con5VD  36985  relopabVD  36986  19.41rgVD  36987  2pm13.193VD  36988  hbimpgVD  36989  hbalgVD  36990  hbexgVD  36991  ax6e2eqVD  36992  ax6e2ndVD  36993  ax6e2ndeqVD  36994  2sb5ndVD  36995  2uasbanhVD  36996  e2ebindVD  36997  sb5ALTVD  36998  vk15.4jVD  36999  notnot2ALTVD  37000  con3ALTVD  37001
  Copyright terms: Public domain W3C validator