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

Theorem e1a 31704
Description: A Virtual deduction elimination rule. syl 16 is e1a 31704 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 31639 . . 3  |-  ( ph  ->  ps )
3 e1a.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 16 . 2  |-  ( ph  ->  ch )
54dfvd1ir 31641 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 31637
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 31638
This theorem is referenced by:  e1bi  31706  e1bir  31707  snelpwrVD  31922  unipwrVD  31923  sstrALT2VD  31925  elex2VD  31929  elex22VD  31930  eqsbc3rVD  31931  zfregs2VD  31932  tpid3gVD  31933  en3lplem1VD  31934  en3lpVD  31936  3ornot23VD  31938  3orbi123VD  31941  sbc3orgVD  31942  exbirVD  31944  3impexpVD  31947  3impexpbicomVD  31948  sbcoreleleqVD  31950  tratrbVD  31952  3ax4VD  31953  syl5impVD  31954  ssralv2VD  31957  ordelordALTVD  31958  sbcim2gVD  31966  trsbcVD  31968  truniALTVD  31969  trintALTVD  31971  undif3VD  31973  sbcssgVD  31974  csbingVD  31975  onfrALTlem3VD  31978  simplbi2comtVD  31979  onfrALTlem2VD  31980  onfrALTVD  31982  csbeq2gVD  31983  csbsngVD  31984  csbxpgVD  31985  csbresgVD  31986  csbrngVD  31987  csbima12gALTVD  31988  csbunigVD  31989  csbfv12gALTVD  31990  con5VD  31991  relopabVD  31992  19.41rgVD  31993  2pm13.193VD  31994  hbimpgVD  31995  hbalgVD  31996  hbexgVD  31997  ax6e2eqVD  31998  ax6e2ndVD  31999  ax6e2ndeqVD  32000  2sb5ndVD  32001  2uasbanhVD  32002  e2ebindVD  32003  sb5ALTVD  32004  vk15.4jVD  32005  notnot2ALTVD  32006  con3ALTVD  32007
  Copyright terms: Public domain W3C validator