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

Theorem e1_ 28629
Description: A Virtual deduction elimination rule. syl 16 is e1_ 28629 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 28563 . . 3  |-  ( ph  ->  ps )
3 e1_.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 16 . 2  |-  ( ph  ->  ch )
54dfvd1ir 28565 1  |-  (. ph  ->.  ch
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28561
This theorem is referenced by:  e1bi  28631  e1bir  28632  snelpwrVD  28844  unipwrVD  28845  sstrALT2VD  28847  elex2VD  28851  elex22VD  28852  eqsbc3rVD  28853  zfregs2VD  28854  tpid3gVD  28855  en3lplem1VD  28856  en3lpVD  28858  3ornot23VD  28860  3orbi123VD  28863  sbc3orgVD  28864  exbirVD  28866  3impexpVD  28869  3impexpbicomVD  28870  sbcoreleleqVD  28872  tratrbVD  28874  3ax5VD  28875  syl5impVD  28876  ssralv2VD  28879  ordelordALTVD  28880  sbcim2gVD  28888  trsbcVD  28890  truniALTVD  28891  trintALTVD  28893  undif3VD  28895  sbcssVD  28896  csbingVD  28897  onfrALTlem3VD  28900  simplbi2comgVD  28901  onfrALTlem2VD  28902  onfrALTVD  28904  csbeq2gVD  28905  csbsngVD  28906  csbxpgVD  28907  csbresgVD  28908  csbrngVD  28909  csbima12gALTVD  28910  csbunigVD  28911  csbfv12gALTVD  28912  con5VD  28913  relopabVD  28914  19.41rgVD  28915  2pm13.193VD  28916  hbimpgVD  28917  hbalgVD  28918  hbexgVD  28919  a9e2eqVD  28920  a9e2ndVD  28921  a9e2ndeqVD  28922  2sb5ndVD  28923  2uasbanhVD  28924  e2ebindVD  28925  sb5ALTVD  28926  vk15.4jVD  28927  notnot2ALTVD  28928  con3ALTVD  28929
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 178  df-vd1 28562
  Copyright terms: Public domain W3C validator