Theorem idn2 42233

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

Syntax hints:  (   wvd2 42197

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 397  df-vd2 42198

This theorem is referenced by:  trsspwALT  42438  sspwtr  42441  pwtrVD  42444  pwtrrVD  42445  snssiALTVD  42447  sstrALT2VD  42454  suctrALT2VD  42456  elex2VD  42458  elex22VD  42459  eqsbc2VD  42460  tpid3gVD  42462  en3lplem1VD  42463  en3lplem2VD  42464  3ornot23VD  42467  orbi1rVD  42468  19.21a3con13vVD  42472  exbirVD  42473  exbiriVD  42474  rspsbc2VD  42475  tratrbVD  42481  syl5impVD  42483  ssralv2VD  42486  imbi12VD  42493  imbi13VD  42494  sbcim2gVD  42495  sbcbiVD  42496  truniALTVD  42498  trintALTVD  42500  onfrALTlem3VD  42507  onfrALTlem2VD  42509  onfrALTlem1VD  42510  relopabVD  42521  19.41rgVD  42522  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndeqVD  42529  sb5ALTVD  42533  vk15.4jVD  42534  con3ALTVD  42536