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

Theorem idn1 39107
Description: Virtual deduction identity rule which is id 22 with virtual deduction symbols. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
idn1 (   𝜑   ▶   𝜑   )

Proof of Theorem idn1
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21dfvd1ir 39106 1 (   𝜑   ▶   𝜑   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd1 39102
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 197  df-vd1 39103
This theorem is referenced by:  trsspwALT  39362  sspwtr  39365  pwtrVD  39373  pwtrrVD  39374  snssiALTVD  39376  snsslVD  39378  snelpwrVD  39380  unipwrVD  39381  sstrALT2VD  39383  suctrALT2VD  39385  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  zfregs2VD  39390  tpid3gVD  39391  en3lplem1VD  39392  en3lplem2VD  39393  en3lpVD  39394  3ornot23VD  39396  orbi1rVD  39397  3orbi123VD  39399  sbc3orgVD  39400  19.21a3con13vVD  39401  exbirVD  39402  exbiriVD  39403  rspsbc2VD  39404  3impexpVD  39405  3impexpbicomVD  39406  sbcoreleleqVD  39409  tratrbVD  39411  al2imVD  39412  syl5impVD  39413  ssralv2VD  39416  ordelordALTVD  39417  equncomVD  39418  imbi12VD  39423  imbi13VD  39424  sbcim2gVD  39425  sbcbiVD  39426  trsbcVD  39427  truniALTVD  39428  trintALTVD  39430  undif3VD  39432  sbcssgVD  39433  csbingVD  39434  onfrALTlem3VD  39437  simplbi2comtVD  39438  onfrALTlem2VD  39439  onfrALTVD  39441  csbeq2gVD  39442  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  relopabVD  39451  19.41rgVD  39452  2pm13.193VD  39453  hbimpgVD  39454  hbalgVD  39455  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndVD  39458  ax6e2ndeqVD  39459  2sb5ndVD  39460  2uasbanhVD  39461  e2ebindVD  39462  sb5ALTVD  39463  vk15.4jVD  39464  notnotrALTVD  39465  con3ALTVD  39466  sspwimpVD  39469  sspwimpcfVD  39471  suctrALTcfVD  39473
  Copyright terms: Public domain W3C validator