Theorem idn2 45350

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

This proof depends on syntax axioms:  (   wvd2 45314

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 401  df-vd2 45315

This theorem is used by:  trsspwALT  45554  sspwtr  45557  pwtrVD  45560  pwtrrVD  45561  snssiALTVD  45563  sstrALT2VD  45570  suctrALT2VD  45572  elex2VD  45574  elex22VD  45575  eqsbc2VD  45576  tpid3gVD  45578  en3lplem1VD  45579  en3lplem2VD  45580  3ornot23VD  45583  orbi1rVD  45584  19.21a3con13vVD  45588  exbirVD  45589  exbiriVD  45590  rspsbc2VD  45591  tratrbVD  45597  syl5impVD  45599  ssralv2VD  45602  imbi12VD  45609  imbi13VD  45610  sbcim2gVD  45611  sbcbiVD  45612  truniALTVD  45614  trintALTVD  45616  onfrALTlem3VD  45623  onfrALTlem2VD  45625  onfrALTlem1VD  45626  relopabVD  45637  19.41rgVD  45638  hbimpgVD  45640  ax6e2eqVD  45643  ax6e2ndeqVD  45645  sb5ALTVD  45649  vk15.4jVD  45650  con3ALTVD  45652