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

Theorem idn1 28641
Description: Virtual deduction identity rule which is id 19 with virtual deduction symbols. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
idn1  |-  (. ph  ->.  ph ).

Proof of Theorem idn1
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
21dfvd1ir 28640 1  |-  (. ph  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28636
This theorem is referenced by:  trsspwALT  28908  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  snssiALTVD  28918  snsslVD  28920  snelpwrVD  28922  unipwrVD  28924  sstrALT2VD  28926  suctrALT2VD  28928  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  zfregs2VD  28933  tpid3gVD  28934  en3lplem1VD  28935  en3lplem2VD  28936  en3lpVD  28937  3ornot23VD  28939  orbi1rVD  28940  3orbi123VD  28942  sbc3orgVD  28943  19.21a3con13vVD  28944  exbirVD  28945  exbiriVD  28946  rspsbc2VD  28947  3impexpVD  28948  3impexpbicomVD  28949  sbcoreleleqVD  28951  tratrbVD  28953  3ax5VD  28954  syl5impVD  28955  ssralv2VD  28958  ordelordALTVD  28959  equncomVD  28960  imbi12VD  28965  imbi13VD  28966  sbcim2gVD  28967  sbcbiVD  28968  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  sspwimpVD  29011  sspwimpcfVD  29013  suctrALTcfVD  29015
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