Theorem idn2 40967

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 40940	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

Syntax hints:  (   wvd2 40931

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-an 399  df-vd2 40932

This theorem is referenced by:  trsspwALT  41172  sspwtr  41175  pwtrVD  41178  pwtrrVD  41179  snssiALTVD  41181  sstrALT2VD  41188  suctrALT2VD  41190  elex2VD  41192  elex22VD  41193  eqsbc3rVD  41194  tpid3gVD  41196  en3lplem1VD  41197  en3lplem2VD  41198  3ornot23VD  41201  orbi1rVD  41202  19.21a3con13vVD  41206  exbirVD  41207  exbiriVD  41208  rspsbc2VD  41209  tratrbVD  41215  syl5impVD  41217  ssralv2VD  41220  imbi12VD  41227  imbi13VD  41228  sbcim2gVD  41229  sbcbiVD  41230  truniALTVD  41232  trintALTVD  41234  onfrALTlem3VD  41241  onfrALTlem2VD  41243  onfrALTlem1VD  41244  relopabVD  41255  19.41rgVD  41256  hbimpgVD  41258  ax6e2eqVD  41261  ax6e2ndeqVD  41263  sb5ALTVD  41267  vk15.4jVD  41268  con3ALTVD  41270