Theorem idn1 44666

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

Syntax hints:  (   wvd1 44661

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 44662

This theorem is referenced by:  trsspwALT  44909  sspwtr  44912  pwtrVD  44915  pwtrrVD  44916  snssiALTVD  44918  snsslVD  44920  snelpwrVD  44922  unipwrVD  44923  sstrALT2VD  44925  suctrALT2VD  44927  elex2VD  44929  elex22VD  44930  eqsbc2VD  44931  zfregs2VD  44932  tpid3gVD  44933  en3lplem1VD  44934  en3lplem2VD  44935  en3lpVD  44936  3ornot23VD  44938  orbi1rVD  44939  3orbi123VD  44941  sbc3orgVD  44942  19.21a3con13vVD  44943  exbirVD  44944  exbiriVD  44945  rspsbc2VD  44946  3impexpVD  44947  3impexpbicomVD  44948  tratrbVD  44952  al2imVD  44953  syl5impVD  44954  ssralv2VD  44957  ordelordALTVD  44958  equncomVD  44959  imbi12VD  44964  imbi13VD  44965  sbcim2gVD  44966  sbcbiVD  44967  trsbcVD  44968  truniALTVD  44969  trintALTVD  44971  undif3VD  44973  sbcssgVD  44974  csbingVD  44975  onfrALTlem3VD  44978  simplbi2comtVD  44979  onfrALTlem2VD  44980  onfrALTVD  44982  csbeq2gVD  44983  csbsngVD  44984  csbxpgVD  44985  csbresgVD  44986  csbrngVD  44987  csbima12gALTVD  44988  csbunigVD  44989  csbfv12gALTVD  44990  con5VD  44991  relopabVD  44992  19.41rgVD  44993  2pm13.193VD  44994  hbimpgVD  44995  hbalgVD  44996  hbexgVD  44997  ax6e2eqVD  44998  ax6e2ndVD  44999  ax6e2ndeqVD  45000  2sb5ndVD  45001  2uasbanhVD  45002  e2ebindVD  45003  sb5ALTVD  45004  vk15.4jVD  45005  notnotrALTVD  45006  con3ALTVD  45007  sspwimpVD  45010  sspwimpcfVD  45012  suctrALTcfVD  45014