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 40898
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 40897 1 (   𝜑   ▶   𝜑   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd1 40893
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 209  df-vd1 40894
This theorem is referenced by:  trsspwALT  41142  sspwtr  41145  pwtrVD  41148  pwtrrVD  41149  snssiALTVD  41151  snsslVD  41153  snelpwrVD  41155  unipwrVD  41156  sstrALT2VD  41158  suctrALT2VD  41160  elex2VD  41162  elex22VD  41163  eqsbc3rVD  41164  zfregs2VD  41165  tpid3gVD  41166  en3lplem1VD  41167  en3lplem2VD  41168  en3lpVD  41169  3ornot23VD  41171  orbi1rVD  41172  3orbi123VD  41174  sbc3orgVD  41175  19.21a3con13vVD  41176  exbirVD  41177  exbiriVD  41178  rspsbc2VD  41179  3impexpVD  41180  3impexpbicomVD  41181  tratrbVD  41185  al2imVD  41186  syl5impVD  41187  ssralv2VD  41190  ordelordALTVD  41191  equncomVD  41192  imbi12VD  41197  imbi13VD  41198  sbcim2gVD  41199  sbcbiVD  41200  trsbcVD  41201  truniALTVD  41202  trintALTVD  41204  undif3VD  41206  sbcssgVD  41207  csbingVD  41208  onfrALTlem3VD  41211  simplbi2comtVD  41212  onfrALTlem2VD  41213  onfrALTVD  41215  csbeq2gVD  41216  csbsngVD  41217  csbxpgVD  41218  csbresgVD  41219  csbrngVD  41220  csbima12gALTVD  41221  csbunigVD  41222  csbfv12gALTVD  41223  con5VD  41224  relopabVD  41225  19.41rgVD  41226  2pm13.193VD  41227  hbimpgVD  41228  hbalgVD  41229  hbexgVD  41230  ax6e2eqVD  41231  ax6e2ndVD  41232  ax6e2ndeqVD  41233  2sb5ndVD  41234  2uasbanhVD  41235  e2ebindVD  41236  sb5ALTVD  41237  vk15.4jVD  41238  notnotrALTVD  41239  con3ALTVD  41240  sspwimpVD  41243  sspwimpcfVD  41245  suctrALTcfVD  41247
  Copyright terms: Public domain W3C validator