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 41306
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 41279 1 (   𝜑   ,   𝜓   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd2 41270
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-an 400  df-vd2 41271
This theorem is referenced by:  trsspwALT  41511  sspwtr  41514  pwtrVD  41517  pwtrrVD  41518  snssiALTVD  41520  sstrALT2VD  41527  suctrALT2VD  41529  elex2VD  41531  elex22VD  41532  eqsbc3rVD  41533  tpid3gVD  41535  en3lplem1VD  41536  en3lplem2VD  41537  3ornot23VD  41540  orbi1rVD  41541  19.21a3con13vVD  41545  exbirVD  41546  exbiriVD  41547  rspsbc2VD  41548  tratrbVD  41554  syl5impVD  41556  ssralv2VD  41559  imbi12VD  41566  imbi13VD  41567  sbcim2gVD  41568  sbcbiVD  41569  truniALTVD  41571  trintALTVD  41573  onfrALTlem3VD  41580  onfrALTlem2VD  41582  onfrALTlem1VD  41583  relopabVD  41594  19.41rgVD  41595  hbimpgVD  41597  ax6e2eqVD  41600  ax6e2ndeqVD  41602  sb5ALTVD  41606  vk15.4jVD  41607  con3ALTVD  41609
  Copyright terms: Public domain W3C validator