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

Theorem e1_ 28399
Description: A Virtual deduction elimination rule. syl 15 is e1_ 28399 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 28339 . . 3  |-  ( ph  ->  ps )
3 e1_.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 15 . 2  |-  ( ph  ->  ch )
54dfvd1ir 28341 1  |-  (. ph  ->.  ch
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337
This theorem is referenced by:  e1bi  28401  e1bir  28402  snelpwrVD  28606  unipwrVD  28608  sstrALT2VD  28610  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  zfregs2VD  28617  tpid3gVD  28618  en3lplem1VD  28619  en3lpVD  28621  3ornot23VD  28623  3orbi123VD  28626  sbc3orgVD  28627  exbirVD  28629  3impexpVD  28632  3impexpbicomVD  28633  sbcoreleleqVD  28635  tratrbVD  28637  3ax5VD  28638  syl5impVD  28639  ssralv2VD  28642  ordelordALTVD  28643  sbcim2gVD  28651  trsbcVD  28653  truniALTVD  28654  trintALTVD  28656  undif3VD  28658  sbcssVD  28659  csbingVD  28660  onfrALTlem3VD  28663  simplbi2comgVD  28664  onfrALTlem2VD  28665  onfrALTVD  28667  csbeq2gVD  28668  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  con5VD  28676  relopabVD  28677  19.41rgVD  28678  2pm13.193VD  28679  hbimpgVD  28680  hbalgVD  28681  hbexgVD  28682  a9e2eqVD  28683  a9e2ndVD  28684  a9e2ndeqVD  28685  2sb5ndVD  28686  2uasbanhVD  28687  e2ebindVD  28688  sb5ALTVD  28689  vk15.4jVD  28690  notnot2ALTVD  28691  con3ALTVD  28692
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 28338
  Copyright terms: Public domain W3C validator