Theorem idn2 45704

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

This proof depends on syntax axioms:  (   wvd2 45668

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 45669

This theorem is used by:  trsspwALT  45908  sspwtr  45911  pwtrVD  45914  pwtrrVD  45915  snssiALTVD  45917  sstrALT2VD  45924  suctrALT2VD  45926  elex2VD  45928  elex22VD  45929  eqsbc2VD  45930  tpid3gVD  45932  en3lplem1VD  45933  en3lplem2VD  45934  3ornot23VD  45937  orbi1rVD  45938  19.21a3con13vVD  45942  exbirVD  45943  exbiriVD  45944  rspsbc2VD  45945  tratrbVD  45951  syl5impVD  45953  ssralv2VD  45956  imbi12VD  45963  imbi13VD  45964  sbcim2gVD  45965  sbcbiVD  45966  truniALTVD  45968  trintALTVD  45970  onfrALTlem3VD  45977  onfrALTlem2VD  45979  onfrALTlem1VD  45980  relopabVD  45991  19.41rgVD  45992  hbimpgVD  45994  ax6e2eqVD  45997  ax6e2ndeqVD  45999  sb5ALTVD  46003  vk15.4jVD  46004  con3ALTVD  46006