Theorem idn1 44672

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

Syntax hints:  (   wvd1 44667

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 44668

This theorem is referenced by:  trsspwALT  44915  sspwtr  44918  pwtrVD  44921  pwtrrVD  44922  snssiALTVD  44924  snsslVD  44926  snelpwrVD  44928  unipwrVD  44929  sstrALT2VD  44931  suctrALT2VD  44933  elex2VD  44935  elex22VD  44936  eqsbc2VD  44937  zfregs2VD  44938  tpid3gVD  44939  en3lplem1VD  44940  en3lplem2VD  44941  en3lpVD  44942  3ornot23VD  44944  orbi1rVD  44945  3orbi123VD  44947  sbc3orgVD  44948  19.21a3con13vVD  44949  exbirVD  44950  exbiriVD  44951  rspsbc2VD  44952  3impexpVD  44953  3impexpbicomVD  44954  tratrbVD  44958  al2imVD  44959  syl5impVD  44960  ssralv2VD  44963  ordelordALTVD  44964  equncomVD  44965  imbi12VD  44970  imbi13VD  44971  sbcim2gVD  44972  sbcbiVD  44973  trsbcVD  44974  truniALTVD  44975  trintALTVD  44977  undif3VD  44979  sbcssgVD  44980  csbingVD  44981  onfrALTlem3VD  44984  simplbi2comtVD  44985  onfrALTlem2VD  44986  onfrALTVD  44988  csbeq2gVD  44989  csbsngVD  44990  csbxpgVD  44991  csbresgVD  44992  csbrngVD  44993  csbima12gALTVD  44994  csbunigVD  44995  csbfv12gALTVD  44996  con5VD  44997  relopabVD  44998  19.41rgVD  44999  2pm13.193VD  45000  hbimpgVD  45001  hbalgVD  45002  hbexgVD  45003  ax6e2eqVD  45004  ax6e2ndVD  45005  ax6e2ndeqVD  45006  2sb5ndVD  45007  2uasbanhVD  45008  e2ebindVD  45009  sb5ALTVD  45010  vk15.4jVD  45011  notnotrALTVD  45012  con3ALTVD  45013  sspwimpVD  45016  sspwimpcfVD  45018  suctrALTcfVD  45020