Theorem idn2 40499

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

Syntax hints:  (   wvd2 40463

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 208  df-an 397  df-vd2 40464

This theorem is referenced by:  trsspwALT  40704  sspwtr  40707  pwtrVD  40710  pwtrrVD  40711  snssiALTVD  40713  sstrALT2VD  40720  suctrALT2VD  40722  elex2VD  40724  elex22VD  40725  eqsbc3rVD  40726  tpid3gVD  40728  en3lplem1VD  40729  en3lplem2VD  40730  3ornot23VD  40733  orbi1rVD  40734  19.21a3con13vVD  40738  exbirVD  40739  exbiriVD  40740  rspsbc2VD  40741  tratrbVD  40747  syl5impVD  40749  ssralv2VD  40752  imbi12VD  40759  imbi13VD  40760  sbcim2gVD  40761  sbcbiVD  40762  truniALTVD  40764  trintALTVD  40766  onfrALTlem3VD  40773  onfrALTlem2VD  40775  onfrALTlem1VD  40776  relopabVD  40787  19.41rgVD  40788  hbimpgVD  40790  ax6e2eqVD  40793  ax6e2ndeqVD  40795  sb5ALTVD  40799  vk15.4jVD  40800  con3ALTVD  40802