Theorem idn1 45746

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

This proof depends on syntax axioms:  (   wvd1 45741

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 45742

This theorem is used by:  trsspwALT  45989  sspwtr  45992  pwtrVD  45995  pwtrrVD  45996  snssiALTVD  45998  snsslVD  46000  snelpwrVD  46002  unipwrVD  46003  sstrALT2VD  46005  suctrALT2VD  46007  elex2VD  46009  elex22VD  46010  eqsbc2VD  46011  zfregs2VD  46012  tpid3gVD  46013  en3lplem1VD  46014  en3lplem2VD  46015  en3lpVD  46016  3ornot23VD  46018  orbi1rVD  46019  3orbi123VD  46021  sbc3orgVD  46022  19.21a3con13vVD  46023  exbirVD  46024  exbiriVD  46025  rspsbc2VD  46026  3impexpVD  46027  3impexpbicomVD  46028  tratrbVD  46032  al2imVD  46033  syl5impVD  46034  ssralv2VD  46037  ordelordALTVD  46038  equncomVD  46039  imbi12VD  46044  imbi13VD  46045  sbcim2gVD  46046  sbcbiVD  46047  trsbcVD  46048  truniALTVD  46049  trintALTVD  46051  undif3VD  46053  sbcssgVD  46054  csbingVD  46055  onfrALTlem3VD  46058  simplbi2comtVD  46059  onfrALTlem2VD  46060  onfrALTVD  46062  csbeq2gVD  46063  csbsngVD  46064  csbxpgVD  46065  csbresgVD  46066  csbrngVD  46067  csbima12gALTVD  46068  csbunigVD  46069  csbfv12gALTVD  46070  con5VD  46071  relopabVD  46072  19.41rgVD  46073  2pm13.193VD  46074  hbimpgVD  46075  hbalgVD  46076  hbexgVD  46077  ax6e2eqVD  46078  ax6e2ndVD  46079  ax6e2ndeqVD  46080  2sb5ndVD  46081  2uasbanhVD  46082  e2ebindVD  46083  sb5ALTVD  46084  vk15.4jVD  46085  notnotrALTVD  46086  con3ALTVD  46087  sspwimpVD  46090  sspwimpcfVD  46092  suctrALTcfVD  46094