Theorem idn1 45031

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

Syntax hints:  (   wvd1 45026

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 45027

This theorem is referenced by:  trsspwALT  45274  sspwtr  45277  pwtrVD  45280  pwtrrVD  45281  snssiALTVD  45283  snsslVD  45285  snelpwrVD  45287  unipwrVD  45288  sstrALT2VD  45290  suctrALT2VD  45292  elex2VD  45294  elex22VD  45295  eqsbc2VD  45296  zfregs2VD  45297  tpid3gVD  45298  en3lplem1VD  45299  en3lplem2VD  45300  en3lpVD  45301  3ornot23VD  45303  orbi1rVD  45304  3orbi123VD  45306  sbc3orgVD  45307  19.21a3con13vVD  45308  exbirVD  45309  exbiriVD  45310  rspsbc2VD  45311  3impexpVD  45312  3impexpbicomVD  45313  tratrbVD  45317  al2imVD  45318  syl5impVD  45319  ssralv2VD  45322  ordelordALTVD  45323  equncomVD  45324  imbi12VD  45329  imbi13VD  45330  sbcim2gVD  45331  sbcbiVD  45332  trsbcVD  45333  truniALTVD  45334  trintALTVD  45336  undif3VD  45338  sbcssgVD  45339  csbingVD  45340  onfrALTlem3VD  45343  simplbi2comtVD  45344  onfrALTlem2VD  45345  onfrALTVD  45347  csbeq2gVD  45348  csbsngVD  45349  csbxpgVD  45350  csbresgVD  45351  csbrngVD  45352  csbima12gALTVD  45353  csbunigVD  45354  csbfv12gALTVD  45355  con5VD  45356  relopabVD  45357  19.41rgVD  45358  2pm13.193VD  45359  hbimpgVD  45360  hbalgVD  45361  hbexgVD  45362  ax6e2eqVD  45363  ax6e2ndVD  45364  ax6e2ndeqVD  45365  2sb5ndVD  45366  2uasbanhVD  45367  e2ebindVD  45368  sb5ALTVD  45369  vk15.4jVD  45370  notnotrALTVD  45371  con3ALTVD  45372  sspwimpVD  45375  sspwimpcfVD  45377  suctrALTcfVD  45379