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 41915
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 41914 1 (   𝜑   ▶   𝜑   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd1 41910
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 210  df-vd1 41911
This theorem is referenced by:  trsspwALT  42159  sspwtr  42162  pwtrVD  42165  pwtrrVD  42166  snssiALTVD  42168  snsslVD  42170  snelpwrVD  42172  unipwrVD  42173  sstrALT2VD  42175  suctrALT2VD  42177  elex2VD  42179  elex22VD  42180  eqsbc2VD  42181  zfregs2VD  42182  tpid3gVD  42183  en3lplem1VD  42184  en3lplem2VD  42185  en3lpVD  42186  3ornot23VD  42188  orbi1rVD  42189  3orbi123VD  42191  sbc3orgVD  42192  19.21a3con13vVD  42193  exbirVD  42194  exbiriVD  42195  rspsbc2VD  42196  3impexpVD  42197  3impexpbicomVD  42198  tratrbVD  42202  al2imVD  42203  syl5impVD  42204  ssralv2VD  42207  ordelordALTVD  42208  equncomVD  42209  imbi12VD  42214  imbi13VD  42215  sbcim2gVD  42216  sbcbiVD  42217  trsbcVD  42218  truniALTVD  42219  trintALTVD  42221  undif3VD  42223  sbcssgVD  42224  csbingVD  42225  onfrALTlem3VD  42228  simplbi2comtVD  42229  onfrALTlem2VD  42230  onfrALTVD  42232  csbeq2gVD  42233  csbsngVD  42234  csbxpgVD  42235  csbresgVD  42236  csbrngVD  42237  csbima12gALTVD  42238  csbunigVD  42239  csbfv12gALTVD  42240  con5VD  42241  relopabVD  42242  19.41rgVD  42243  2pm13.193VD  42244  hbimpgVD  42245  hbalgVD  42246  hbexgVD  42247  ax6e2eqVD  42248  ax6e2ndVD  42249  ax6e2ndeqVD  42250  2sb5ndVD  42251  2uasbanhVD  42252  e2ebindVD  42253  sb5ALTVD  42254  vk15.4jVD  42255  notnotrALTVD  42256  con3ALTVD  42257  sspwimpVD  42260  sspwimpcfVD  42262  suctrALTcfVD  42264
  Copyright terms: Public domain W3C validator