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 39524
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 39488 1 (   𝜑   ,   𝜓   ▶   𝜓   )
Colors of variables: wff setvar class
Syntax hints:  (   wvd2 39479
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 198  df-an 385  df-vd2 39480
This theorem is referenced by:  trsspwALT  39730  sspwtr  39733  pwtrVD  39736  pwtrrVD  39737  snssiALTVD  39739  sstrALT2VD  39746  suctrALT2VD  39748  elex2VD  39750  elex22VD  39751  eqsbc3rVD  39752  tpid3gVD  39754  en3lplem1VD  39755  en3lplem2VD  39756  3ornot23VD  39759  orbi1rVD  39760  19.21a3con13vVD  39764  exbirVD  39765  exbiriVD  39766  rspsbc2VD  39767  tratrbVD  39773  syl5impVD  39775  ssralv2VD  39778  imbi12VD  39785  imbi13VD  39786  sbcim2gVD  39787  sbcbiVD  39788  truniALTVD  39790  trintALTVD  39792  onfrALTlem3VD  39799  onfrALTlem2VD  39801  onfrALTlem1VD  39802  relopabVD  39813  19.41rgVD  39814  hbimpgVD  39816  ax6e2eqVD  39819  ax6e2ndeqVD  39821  sb5ALTVD  39825  vk15.4jVD  39826  con3ALTVD  39828
  Copyright terms: Public domain W3C validator