Theorem idn2 44796

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

Syntax hints:  (   wvd2 44760

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 207  df-an 396  df-vd2 44761

This theorem is referenced by:  trsspwALT  45000  sspwtr  45003  pwtrVD  45006  pwtrrVD  45007  snssiALTVD  45009  sstrALT2VD  45016  suctrALT2VD  45018  elex2VD  45020  elex22VD  45021  eqsbc2VD  45022  tpid3gVD  45024  en3lplem1VD  45025  en3lplem2VD  45026  3ornot23VD  45029  orbi1rVD  45030  19.21a3con13vVD  45034  exbirVD  45035  exbiriVD  45036  rspsbc2VD  45037  tratrbVD  45043  syl5impVD  45045  ssralv2VD  45048  imbi12VD  45055  imbi13VD  45056  sbcim2gVD  45057  sbcbiVD  45058  truniALTVD  45060  trintALTVD  45062  onfrALTlem3VD  45069  onfrALTlem2VD  45071  onfrALTlem1VD  45072  relopabVD  45083  19.41rgVD  45084  hbimpgVD  45086  ax6e2eqVD  45089  ax6e2ndeqVD  45091  sb5ALTVD  45095  vk15.4jVD  45096  con3ALTVD  45098