Theorem idn1 44568

Description: Virtual deduction identity rule which is id 22 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 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	dfvd1ir 44567	1 ⊢ (   𝜑   ▶   𝜑   )

Syntax hints:  (   wvd1 44563

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 207  df-vd1 44564

This theorem is referenced by:  trsspwALT  44811  sspwtr  44814  pwtrVD  44817  pwtrrVD  44818  snssiALTVD  44820  snsslVD  44822  snelpwrVD  44824  unipwrVD  44825  sstrALT2VD  44827  suctrALT2VD  44829  elex2VD  44831  elex22VD  44832  eqsbc2VD  44833  zfregs2VD  44834  tpid3gVD  44835  en3lplem1VD  44836  en3lplem2VD  44837  en3lpVD  44838  3ornot23VD  44840  orbi1rVD  44841  3orbi123VD  44843  sbc3orgVD  44844  19.21a3con13vVD  44845  exbirVD  44846  exbiriVD  44847  rspsbc2VD  44848  3impexpVD  44849  3impexpbicomVD  44850  tratrbVD  44854  al2imVD  44855  syl5impVD  44856  ssralv2VD  44859  ordelordALTVD  44860  equncomVD  44861  imbi12VD  44866  imbi13VD  44867  sbcim2gVD  44868  sbcbiVD  44869  trsbcVD  44870  truniALTVD  44871  trintALTVD  44873  undif3VD  44875  sbcssgVD  44876  csbingVD  44877  onfrALTlem3VD  44880  simplbi2comtVD  44881  onfrALTlem2VD  44882  onfrALTVD  44884  csbeq2gVD  44885  csbsngVD  44886  csbxpgVD  44887  csbresgVD  44888  csbrngVD  44889  csbima12gALTVD  44890  csbunigVD  44891  csbfv12gALTVD  44892  con5VD  44893  relopabVD  44894  19.41rgVD  44895  2pm13.193VD  44896  hbimpgVD  44897  hbalgVD  44898  hbexgVD  44899  ax6e2eqVD  44900  ax6e2ndVD  44901  ax6e2ndeqVD  44902  2sb5ndVD  44903  2uasbanhVD  44904  e2ebindVD  44905  sb5ALTVD  44906  vk15.4jVD  44907  notnotrALTVD  44908  con3ALTVD  44909  sspwimpVD  44912  sspwimpcfVD  44914  suctrALTcfVD  44916