Theorem idn2 43374

Description: Virtual deduction identity rule which is idd 24 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 24	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2	1	dfvd2ir 43347	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

Syntax hints:  (   wvd2 43338

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 206  df-an 398  df-vd2 43339

This theorem is referenced by:  trsspwALT  43579  sspwtr  43582  pwtrVD  43585  pwtrrVD  43586  snssiALTVD  43588  sstrALT2VD  43595  suctrALT2VD  43597  elex2VD  43599  elex22VD  43600  eqsbc2VD  43601  tpid3gVD  43603  en3lplem1VD  43604  en3lplem2VD  43605  3ornot23VD  43608  orbi1rVD  43609  19.21a3con13vVD  43613  exbirVD  43614  exbiriVD  43615  rspsbc2VD  43616  tratrbVD  43622  syl5impVD  43624  ssralv2VD  43627  imbi12VD  43634  imbi13VD  43635  sbcim2gVD  43636  sbcbiVD  43637  truniALTVD  43639  trintALTVD  43641  onfrALTlem3VD  43648  onfrALTlem2VD  43650  onfrALTlem1VD  43651  relopabVD  43662  19.41rgVD  43663  hbimpgVD  43665  ax6e2eqVD  43668  ax6e2ndeqVD  43670  sb5ALTVD  43674  vk15.4jVD  43675  con3ALTVD  43677