Theorem idn1 45311

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

This proof depends on syntax axioms:  (   wvd1 45306

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 45307

This theorem is used by:  trsspwALT  45554  sspwtr  45557  pwtrVD  45560  pwtrrVD  45561  snssiALTVD  45563  snsslVD  45565  snelpwrVD  45567  unipwrVD  45568  sstrALT2VD  45570  suctrALT2VD  45572  elex2VD  45574  elex22VD  45575  eqsbc2VD  45576  zfregs2VD  45577  tpid3gVD  45578  en3lplem1VD  45579  en3lplem2VD  45580  en3lpVD  45581  3ornot23VD  45583  orbi1rVD  45584  3orbi123VD  45586  sbc3orgVD  45587  19.21a3con13vVD  45588  exbirVD  45589  exbiriVD  45590  rspsbc2VD  45591  3impexpVD  45592  3impexpbicomVD  45593  tratrbVD  45597  al2imVD  45598  syl5impVD  45599  ssralv2VD  45602  ordelordALTVD  45603  equncomVD  45604  imbi12VD  45609  imbi13VD  45610  sbcim2gVD  45611  sbcbiVD  45612  trsbcVD  45613  truniALTVD  45614  trintALTVD  45616  undif3VD  45618  sbcssgVD  45619  csbingVD  45620  onfrALTlem3VD  45623  simplbi2comtVD  45624  onfrALTlem2VD  45625  onfrALTVD  45627  csbeq2gVD  45628  csbsngVD  45629  csbxpgVD  45630  csbresgVD  45631  csbrngVD  45632  csbima12gALTVD  45633  csbunigVD  45634  csbfv12gALTVD  45635  con5VD  45636  relopabVD  45637  19.41rgVD  45638  2pm13.193VD  45639  hbimpgVD  45640  hbalgVD  45641  hbexgVD  45642  ax6e2eqVD  45643  ax6e2ndVD  45644  ax6e2ndeqVD  45645  2sb5ndVD  45646  2uasbanhVD  45647  e2ebindVD  45648  sb5ALTVD  45649  vk15.4jVD  45650  notnotrALTVD  45651  con3ALTVD  45652  sspwimpVD  45655  sspwimpcfVD  45657  suctrALTcfVD  45659