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

Theorem idn2 39155
Description: Virtual deduction identity rule which is idd 24 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
idn2 (   𝜑   ,   𝜓   ▶   𝜓   )

Proof of Theorem idn2
StepHypRef Expression
1 idd 24 . 2 (𝜑 → (𝜓𝜓))
21dfvd2ir 39119 1 (   𝜑   ,   𝜓   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd2 39110
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-an 385  df-vd2 39111
This theorem is referenced by:  trsspwALT  39362  sspwtr  39365  pwtrVD  39373  pwtrrVD  39374  snssiALTVD  39376  sstrALT2VD  39383  suctrALT2VD  39385  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  tpid3gVD  39391  en3lplem1VD  39392  en3lplem2VD  39393  3ornot23VD  39396  orbi1rVD  39397  19.21a3con13vVD  39401  exbirVD  39402  exbiriVD  39403  rspsbc2VD  39404  tratrbVD  39411  syl5impVD  39413  ssralv2VD  39416  imbi12VD  39423  imbi13VD  39424  sbcim2gVD  39425  sbcbiVD  39426  truniALTVD  39428  trintALTVD  39430  onfrALTlem3VD  39437  onfrALTlem2VD  39439  onfrALTlem1VD  39440  relopabVD  39451  19.41rgVD  39452  hbimpgVD  39454  ax6e2eqVD  39457  ax6e2ndeqVD  39459  sb5ALTVD  39463  vk15.4jVD  39464  con3ALTVD  39466
  Copyright terms: Public domain W3C validator