Theorem idn1 44564

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

Syntax hints:  (   wvd1 44559

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 44560

This theorem is referenced by:  trsspwALT  44807  sspwtr  44810  pwtrVD  44813  pwtrrVD  44814  snssiALTVD  44816  snsslVD  44818  snelpwrVD  44820  unipwrVD  44821  sstrALT2VD  44823  suctrALT2VD  44825  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  zfregs2VD  44830  tpid3gVD  44831  en3lplem1VD  44832  en3lplem2VD  44833  en3lpVD  44834  3ornot23VD  44836  orbi1rVD  44837  3orbi123VD  44839  sbc3orgVD  44840  19.21a3con13vVD  44841  exbirVD  44842  exbiriVD  44843  rspsbc2VD  44844  3impexpVD  44845  3impexpbicomVD  44846  tratrbVD  44850  al2imVD  44851  syl5impVD  44852  ssralv2VD  44855  ordelordALTVD  44856  equncomVD  44857  imbi12VD  44862  imbi13VD  44863  sbcim2gVD  44864  sbcbiVD  44865  trsbcVD  44866  truniALTVD  44867  trintALTVD  44869  undif3VD  44871  sbcssgVD  44872  csbingVD  44873  onfrALTlem3VD  44876  simplbi2comtVD  44877  onfrALTlem2VD  44878  onfrALTVD  44880  csbeq2gVD  44881  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  con5VD  44889  relopabVD  44890  19.41rgVD  44891  2pm13.193VD  44892  hbimpgVD  44893  hbalgVD  44894  hbexgVD  44895  ax6e2eqVD  44896  ax6e2ndVD  44897  ax6e2ndeqVD  44898  2sb5ndVD  44899  2uasbanhVD  44900  e2ebindVD  44901  sb5ALTVD  44902  vk15.4jVD  44903  notnotrALTVD  44904  con3ALTVD  44905  sspwimpVD  44908  sspwimpcfVD  44910  suctrALTcfVD  44912