Theorem idn1 45557

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

This proof depends on syntax axioms:  (   wvd1 45552

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 45553

This theorem is used by:  trsspwALT  45800  sspwtr  45803  pwtrVD  45806  pwtrrVD  45807  snssiALTVD  45809  snsslVD  45811  snelpwrVD  45813  unipwrVD  45814  sstrALT2VD  45816  suctrALT2VD  45818  elex2VD  45820  elex22VD  45821  eqsbc2VD  45822  zfregs2VD  45823  tpid3gVD  45824  en3lplem1VD  45825  en3lplem2VD  45826  en3lpVD  45827  3ornot23VD  45829  orbi1rVD  45830  3orbi123VD  45832  sbc3orgVD  45833  19.21a3con13vVD  45834  exbirVD  45835  exbiriVD  45836  rspsbc2VD  45837  3impexpVD  45838  3impexpbicomVD  45839  tratrbVD  45843  al2imVD  45844  syl5impVD  45845  ssralv2VD  45848  ordelordALTVD  45849  equncomVD  45850  imbi12VD  45855  imbi13VD  45856  sbcim2gVD  45857  sbcbiVD  45858  trsbcVD  45859  truniALTVD  45860  trintALTVD  45862  undif3VD  45864  sbcssgVD  45865  csbingVD  45866  onfrALTlem3VD  45869  simplbi2comtVD  45870  onfrALTlem2VD  45871  onfrALTVD  45873  csbeq2gVD  45874  csbsngVD  45875  csbxpgVD  45876  csbresgVD  45877  csbrngVD  45878  csbima12gALTVD  45879  csbunigVD  45880  csbfv12gALTVD  45881  con5VD  45882  relopabVD  45883  19.41rgVD  45884  2pm13.193VD  45885  hbimpgVD  45886  hbalgVD  45887  hbexgVD  45888  ax6e2eqVD  45889  ax6e2ndVD  45890  ax6e2ndeqVD  45891  2sb5ndVD  45892  2uasbanhVD  45893  e2ebindVD  45894  sb5ALTVD  45895  vk15.4jVD  45896  notnotrALTVD  45897  con3ALTVD  45898  sspwimpVD  45901  sspwimpcfVD  45903  suctrALTcfVD  45905