Theorem idn1 43335

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

Syntax hints:  (   wvd1 43330

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 206  df-vd1 43331

This theorem is referenced by:  trsspwALT  43579  sspwtr  43582  pwtrVD  43585  pwtrrVD  43586  snssiALTVD  43588  snsslVD  43590  snelpwrVD  43592  unipwrVD  43593  sstrALT2VD  43595  suctrALT2VD  43597  elex2VD  43599  elex22VD  43600  eqsbc2VD  43601  zfregs2VD  43602  tpid3gVD  43603  en3lplem1VD  43604  en3lplem2VD  43605  en3lpVD  43606  3ornot23VD  43608  orbi1rVD  43609  3orbi123VD  43611  sbc3orgVD  43612  19.21a3con13vVD  43613  exbirVD  43614  exbiriVD  43615  rspsbc2VD  43616  3impexpVD  43617  3impexpbicomVD  43618  tratrbVD  43622  al2imVD  43623  syl5impVD  43624  ssralv2VD  43627  ordelordALTVD  43628  equncomVD  43629  imbi12VD  43634  imbi13VD  43635  sbcim2gVD  43636  sbcbiVD  43637  trsbcVD  43638  truniALTVD  43639  trintALTVD  43641  undif3VD  43643  sbcssgVD  43644  csbingVD  43645  onfrALTlem3VD  43648  simplbi2comtVD  43649  onfrALTlem2VD  43650  onfrALTVD  43652  csbeq2gVD  43653  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  con5VD  43661  relopabVD  43662  19.41rgVD  43663  2pm13.193VD  43664  hbimpgVD  43665  hbalgVD  43666  hbexgVD  43667  ax6e2eqVD  43668  ax6e2ndVD  43669  ax6e2ndeqVD  43670  2sb5ndVD  43671  2uasbanhVD  43672  e2ebindVD  43673  sb5ALTVD  43674  vk15.4jVD  43675  notnotrALTVD  43676  con3ALTVD  43677  sspwimpVD  43680  sspwimpcfVD  43682  suctrALTcfVD  43684