Theorem idn1 45495

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 45494	1 ⊢ (   𝜑   ▶   𝜑   )

This proof depends on syntax axioms:  (   wvd1 45490

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45491

This theorem is used by:  trsspwALT  45738  sspwtr  45741  pwtrVD  45744  pwtrrVD  45745  snssiALTVD  45747  snsslVD  45749  snelpwrVD  45751  unipwrVD  45752  sstrALT2VD  45754  suctrALT2VD  45756  elex2VD  45758  elex22VD  45759  eqsbc2VD  45760  zfregs2VD  45761  tpid3gVD  45762  en3lplem1VD  45763  en3lplem2VD  45764  en3lpVD  45765  3ornot23VD  45767  orbi1rVD  45768  3orbi123VD  45770  sbc3orgVD  45771  19.21a3con13vVD  45772  exbirVD  45773  exbiriVD  45774  rspsbc2VD  45775  3impexpVD  45776  3impexpbicomVD  45777  tratrbVD  45781  al2imVD  45782  syl5impVD  45783  ssralv2VD  45786  ordelordALTVD  45787  equncomVD  45788  imbi12VD  45793  imbi13VD  45794  sbcim2gVD  45795  sbcbiVD  45796  trsbcVD  45797  truniALTVD  45798  trintALTVD  45800  undif3VD  45802  sbcssgVD  45803  csbingVD  45804  onfrALTlem3VD  45807  simplbi2comtVD  45808  onfrALTlem2VD  45809  onfrALTVD  45811  csbeq2gVD  45812  csbsngVD  45813  csbxpgVD  45814  csbresgVD  45815  csbrngVD  45816  csbima12gALTVD  45817  csbunigVD  45818  csbfv12gALTVD  45819  con5VD  45820  relopabVD  45821  19.41rgVD  45822  2pm13.193VD  45823  hbimpgVD  45824  hbalgVD  45825  hbexgVD  45826  ax6e2eqVD  45827  ax6e2ndVD  45828  ax6e2ndeqVD  45829  2sb5ndVD  45830  2uasbanhVD  45831  e2ebindVD  45832  sb5ALTVD  45833  vk15.4jVD  45834  notnotrALTVD  45835  con3ALTVD  45836  sspwimpVD  45839  sspwimpcfVD  45841  suctrALTcfVD  45843