Theorem idn1 45316

Description: Virtual deduction identity rule which is id 23 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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	dfvd1ir 45315	1 ⊢ (   𝜑   ▶   𝜑   )

This proof depends on syntax axioms:  (   wvd1 45311

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45312

This theorem is used by:  trsspwALT  45559  sspwtr  45562  pwtrVD  45565  pwtrrVD  45566  snssiALTVD  45568  snsslVD  45570  snelpwrVD  45572  unipwrVD  45573  sstrALT2VD  45575  suctrALT2VD  45577  elex2VD  45579  elex22VD  45580  eqsbc2VD  45581  zfregs2VD  45582  tpid3gVD  45583  en3lplem1VD  45584  en3lplem2VD  45585  en3lpVD  45586  3ornot23VD  45588  orbi1rVD  45589  3orbi123VD  45591  sbc3orgVD  45592  19.21a3con13vVD  45593  exbirVD  45594  exbiriVD  45595  rspsbc2VD  45596  3impexpVD  45597  3impexpbicomVD  45598  tratrbVD  45602  al2imVD  45603  syl5impVD  45604  ssralv2VD  45607  ordelordALTVD  45608  equncomVD  45609  imbi12VD  45614  imbi13VD  45615  sbcim2gVD  45616  sbcbiVD  45617  trsbcVD  45618  truniALTVD  45619  trintALTVD  45621  undif3VD  45623  sbcssgVD  45624  csbingVD  45625  onfrALTlem3VD  45628  simplbi2comtVD  45629  onfrALTlem2VD  45630  onfrALTVD  45632  csbeq2gVD  45633  csbsngVD  45634  csbxpgVD  45635  csbresgVD  45636  csbrngVD  45637  csbima12gALTVD  45638  csbunigVD  45639  csbfv12gALTVD  45640  con5VD  45641  relopabVD  45642  19.41rgVD  45643  2pm13.193VD  45644  hbimpgVD  45645  hbalgVD  45646  hbexgVD  45647  ax6e2eqVD  45648  ax6e2ndVD  45649  ax6e2ndeqVD  45650  2sb5ndVD  45651  2uasbanhVD  45652  e2ebindVD  45653  sb5ALTVD  45654  vk15.4jVD  45655  notnotrALTVD  45656  con3ALTVD  45657  sspwimpVD  45660  sspwimpcfVD  45662  suctrALTcfVD  45664