Theorem idn1 45155

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

Syntax hints:  (   wvd1 45150

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 209  df-vd1 45151

This theorem is referenced by:  trsspwALT  45398  sspwtr  45401  pwtrVD  45404  pwtrrVD  45405  snssiALTVD  45407  snsslVD  45409  snelpwrVD  45411  unipwrVD  45412  sstrALT2VD  45414  suctrALT2VD  45416  elex2VD  45418  elex22VD  45419  eqsbc2VD  45420  zfregs2VD  45421  tpid3gVD  45422  en3lplem1VD  45423  en3lplem2VD  45424  en3lpVD  45425  3ornot23VD  45427  orbi1rVD  45428  3orbi123VD  45430  sbc3orgVD  45431  19.21a3con13vVD  45432  exbirVD  45433  exbiriVD  45434  rspsbc2VD  45435  3impexpVD  45436  3impexpbicomVD  45437  tratrbVD  45441  al2imVD  45442  syl5impVD  45443  ssralv2VD  45446  ordelordALTVD  45447  equncomVD  45448  imbi12VD  45453  imbi13VD  45454  sbcim2gVD  45455  sbcbiVD  45456  trsbcVD  45457  truniALTVD  45458  trintALTVD  45460  undif3VD  45462  sbcssgVD  45463  csbingVD  45464  onfrALTlem3VD  45467  simplbi2comtVD  45468  onfrALTlem2VD  45469  onfrALTVD  45471  csbeq2gVD  45472  csbsngVD  45473  csbxpgVD  45474  csbresgVD  45475  csbrngVD  45476  csbima12gALTVD  45477  csbunigVD  45478  csbfv12gALTVD  45479  con5VD  45480  relopabVD  45481  19.41rgVD  45482  2pm13.193VD  45483  hbimpgVD  45484  hbalgVD  45485  hbexgVD  45486  ax6e2eqVD  45487  ax6e2ndVD  45488  ax6e2ndeqVD  45489  2sb5ndVD  45490  2uasbanhVD  45491  e2ebindVD  45492  sb5ALTVD  45493  vk15.4jVD  45494  notnotrALTVD  45495  con3ALTVD  45496  sspwimpVD  45499  sspwimpcfVD  45501  suctrALTcfVD  45503