Theorem idn2 44854

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

Syntax hints:  (   wvd2 44818

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 44819

This theorem is referenced by:  trsspwALT  45058  sspwtr  45061  pwtrVD  45064  pwtrrVD  45065  snssiALTVD  45067  sstrALT2VD  45074  suctrALT2VD  45076  elex2VD  45078  elex22VD  45079  eqsbc2VD  45080  tpid3gVD  45082  en3lplem1VD  45083  en3lplem2VD  45084  3ornot23VD  45087  orbi1rVD  45088  19.21a3con13vVD  45092  exbirVD  45093  exbiriVD  45094  rspsbc2VD  45095  tratrbVD  45101  syl5impVD  45103  ssralv2VD  45106  imbi12VD  45113  imbi13VD  45114  sbcim2gVD  45115  sbcbiVD  45116  truniALTVD  45118  trintALTVD  45120  onfrALTlem3VD  45127  onfrALTlem2VD  45129  onfrALTlem1VD  45130  relopabVD  45141  19.41rgVD  45142  hbimpgVD  45144  ax6e2eqVD  45147  ax6e2ndeqVD  45149  sb5ALTVD  45153  vk15.4jVD  45154  con3ALTVD  45156