Theorem idn2 45322

Description: Virtual deduction identity rule which is idd 25 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
idn2	⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

Proof of Theorem idn2

Step	Hyp	Ref	Expression
1		idd 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2	1	dfvd2ir 45295	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

Syntax hints:  (   wvd2 45286

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 210  df-an 401  df-vd2 45287

This theorem is referenced by:  trsspwALT  45526  sspwtr  45529  pwtrVD  45532  pwtrrVD  45533  snssiALTVD  45535  sstrALT2VD  45542  suctrALT2VD  45544  elex2VD  45546  elex22VD  45547  eqsbc2VD  45548  tpid3gVD  45550  en3lplem1VD  45551  en3lplem2VD  45552  3ornot23VD  45555  orbi1rVD  45556  19.21a3con13vVD  45560  exbirVD  45561  exbiriVD  45562  rspsbc2VD  45563  tratrbVD  45569  syl5impVD  45571  ssralv2VD  45574  imbi12VD  45581  imbi13VD  45582  sbcim2gVD  45583  sbcbiVD  45584  truniALTVD  45586  trintALTVD  45588  onfrALTlem3VD  45595  onfrALTlem2VD  45597  onfrALTlem1VD  45598  relopabVD  45609  19.41rgVD  45610  hbimpgVD  45612  ax6e2eqVD  45615  ax6e2ndeqVD  45617  sb5ALTVD  45621  vk15.4jVD  45622  con3ALTVD  45624