Theorem idn2 45380

Description: Virtual deduction identity rule which is idd 25 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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2	1	dfvd2ir 45353	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

This proof depends on syntax axioms:  (   wvd2 45344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd2 45345

This theorem is used by:  trsspwALT  45584  sspwtr  45587  pwtrVD  45590  pwtrrVD  45591  snssiALTVD  45593  sstrALT2VD  45600  suctrALT2VD  45602  elex2VD  45604  elex22VD  45605  eqsbc2VD  45606  tpid3gVD  45608  en3lplem1VD  45609  en3lplem2VD  45610  3ornot23VD  45613  orbi1rVD  45614  19.21a3con13vVD  45618  exbirVD  45619  exbiriVD  45620  rspsbc2VD  45621  tratrbVD  45627  syl5impVD  45629  ssralv2VD  45632  imbi12VD  45639  imbi13VD  45640  sbcim2gVD  45641  sbcbiVD  45642  truniALTVD  45644  trintALTVD  45646  onfrALTlem3VD  45653  onfrALTlem2VD  45655  onfrALTlem1VD  45656  relopabVD  45667  19.41rgVD  45668  hbimpgVD  45670  ax6e2eqVD  45673  ax6e2ndeqVD  45675  sb5ALTVD  45679  vk15.4jVD  45680  con3ALTVD  45682