Theorem idn2 44654

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

Syntax hints:  (   wvd2 44618

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 44619

This theorem is referenced by:  trsspwALT  44858  sspwtr  44861  pwtrVD  44864  pwtrrVD  44865  snssiALTVD  44867  sstrALT2VD  44874  suctrALT2VD  44876  elex2VD  44878  elex22VD  44879  eqsbc2VD  44880  tpid3gVD  44882  en3lplem1VD  44883  en3lplem2VD  44884  3ornot23VD  44887  orbi1rVD  44888  19.21a3con13vVD  44892  exbirVD  44893  exbiriVD  44894  rspsbc2VD  44895  tratrbVD  44901  syl5impVD  44903  ssralv2VD  44906  imbi12VD  44913  imbi13VD  44914  sbcim2gVD  44915  sbcbiVD  44916  truniALTVD  44918  trintALTVD  44920  onfrALTlem3VD  44927  onfrALTlem2VD  44929  onfrALTlem1VD  44930  relopabVD  44941  19.41rgVD  44942  hbimpgVD  44944  ax6e2eqVD  44947  ax6e2ndeqVD  44949  sb5ALTVD  44953  vk15.4jVD  44954  con3ALTVD  44956