Theorem idn1 45231

Description: Virtual deduction identity rule which is id 23 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

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	dfvd1ir 45230	1 ⊢ (   𝜑   ▶   𝜑   )

Syntax hints:  (   wvd1 45226

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 45227

This theorem is referenced by:  trsspwALT  45474  sspwtr  45477  pwtrVD  45480  pwtrrVD  45481  snssiALTVD  45483  snsslVD  45485  snelpwrVD  45487  unipwrVD  45488  sstrALT2VD  45490  suctrALT2VD  45492  elex2VD  45494  elex22VD  45495  eqsbc2VD  45496  zfregs2VD  45497  tpid3gVD  45498  en3lplem1VD  45499  en3lplem2VD  45500  en3lpVD  45501  3ornot23VD  45503  orbi1rVD  45504  3orbi123VD  45506  sbc3orgVD  45507  19.21a3con13vVD  45508  exbirVD  45509  exbiriVD  45510  rspsbc2VD  45511  3impexpVD  45512  3impexpbicomVD  45513  tratrbVD  45517  al2imVD  45518  syl5impVD  45519  ssralv2VD  45522  ordelordALTVD  45523  equncomVD  45524  imbi12VD  45529  imbi13VD  45530  sbcim2gVD  45531  sbcbiVD  45532  trsbcVD  45533  truniALTVD  45534  trintALTVD  45536  undif3VD  45538  sbcssgVD  45539  csbingVD  45540  onfrALTlem3VD  45543  simplbi2comtVD  45544  onfrALTlem2VD  45545  onfrALTVD  45547  csbeq2gVD  45548  csbsngVD  45549  csbxpgVD  45550  csbresgVD  45551  csbrngVD  45552  csbima12gALTVD  45553  csbunigVD  45554  csbfv12gALTVD  45555  con5VD  45556  relopabVD  45557  19.41rgVD  45558  2pm13.193VD  45559  hbimpgVD  45560  hbalgVD  45561  hbexgVD  45562  ax6e2eqVD  45563  ax6e2ndVD  45564  ax6e2ndeqVD  45565  2sb5ndVD  45566  2uasbanhVD  45567  e2ebindVD  45568  sb5ALTVD  45569  vk15.4jVD  45570  notnotrALTVD  45571  con3ALTVD  45572  sspwimpVD  45575  sspwimpcfVD  45577  suctrALTcfVD  45579