Theorem idn1 44574

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

Syntax hints:  (   wvd1 44569

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 44570

This theorem is referenced by:  trsspwALT  44817  sspwtr  44820  pwtrVD  44823  pwtrrVD  44824  snssiALTVD  44826  snsslVD  44828  snelpwrVD  44830  unipwrVD  44831  sstrALT2VD  44833  suctrALT2VD  44835  elex2VD  44837  elex22VD  44838  eqsbc2VD  44839  zfregs2VD  44840  tpid3gVD  44841  en3lplem1VD  44842  en3lplem2VD  44843  en3lpVD  44844  3ornot23VD  44846  orbi1rVD  44847  3orbi123VD  44849  sbc3orgVD  44850  19.21a3con13vVD  44851  exbirVD  44852  exbiriVD  44853  rspsbc2VD  44854  3impexpVD  44855  3impexpbicomVD  44856  tratrbVD  44860  al2imVD  44861  syl5impVD  44862  ssralv2VD  44865  ordelordALTVD  44866  equncomVD  44867  imbi12VD  44872  imbi13VD  44873  sbcim2gVD  44874  sbcbiVD  44875  trsbcVD  44876  truniALTVD  44877  trintALTVD  44879  undif3VD  44881  sbcssgVD  44882  csbingVD  44883  onfrALTlem3VD  44886  simplbi2comtVD  44887  onfrALTlem2VD  44888  onfrALTVD  44890  csbeq2gVD  44891  csbsngVD  44892  csbxpgVD  44893  csbresgVD  44894  csbrngVD  44895  csbima12gALTVD  44896  csbunigVD  44897  csbfv12gALTVD  44898  con5VD  44899  relopabVD  44900  19.41rgVD  44901  2pm13.193VD  44902  hbimpgVD  44903  hbalgVD  44904  hbexgVD  44905  ax6e2eqVD  44906  ax6e2ndVD  44907  ax6e2ndeqVD  44908  2sb5ndVD  44909  2uasbanhVD  44910  e2ebindVD  44911  sb5ALTVD  44912  vk15.4jVD  44913  notnotrALTVD  44914  con3ALTVD  44915  sspwimpVD  44918  sspwimpcfVD  44920  suctrALTcfVD  44922