Theorem idn1 44599

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

Syntax hints:  (   wvd1 44594

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 44595

This theorem is referenced by:  trsspwALT  44843  sspwtr  44846  pwtrVD  44849  pwtrrVD  44850  snssiALTVD  44852  snsslVD  44854  snelpwrVD  44856  unipwrVD  44857  sstrALT2VD  44859  suctrALT2VD  44861  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  zfregs2VD  44866  tpid3gVD  44867  en3lplem1VD  44868  en3lplem2VD  44869  en3lpVD  44870  3ornot23VD  44872  orbi1rVD  44873  3orbi123VD  44875  sbc3orgVD  44876  19.21a3con13vVD  44877  exbirVD  44878  exbiriVD  44879  rspsbc2VD  44880  3impexpVD  44881  3impexpbicomVD  44882  tratrbVD  44886  al2imVD  44887  syl5impVD  44888  ssralv2VD  44891  ordelordALTVD  44892  equncomVD  44893  imbi12VD  44898  imbi13VD  44899  sbcim2gVD  44900  sbcbiVD  44901  trsbcVD  44902  truniALTVD  44903  trintALTVD  44905  undif3VD  44907  sbcssgVD  44908  csbingVD  44909  onfrALTlem3VD  44912  simplbi2comtVD  44913  onfrALTlem2VD  44914  onfrALTVD  44916  csbeq2gVD  44917  csbsngVD  44918  csbxpgVD  44919  csbresgVD  44920  csbrngVD  44921  csbima12gALTVD  44922  csbunigVD  44923  csbfv12gALTVD  44924  con5VD  44925  relopabVD  44926  19.41rgVD  44927  2pm13.193VD  44928  hbimpgVD  44929  hbalgVD  44930  hbexgVD  44931  ax6e2eqVD  44932  ax6e2ndVD  44933  ax6e2ndeqVD  44934  2sb5ndVD  44935  2uasbanhVD  44936  e2ebindVD  44937  sb5ALTVD  44938  vk15.4jVD  44939  notnotrALTVD  44940  con3ALTVD  44941  sspwimpVD  44944  sspwimpcfVD  44946  suctrALTcfVD  44948