Theorem idn2 45061

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

Syntax hints:  (   wvd2 45025

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 45026

This theorem is referenced by:  trsspwALT  45265  sspwtr  45268  pwtrVD  45271  pwtrrVD  45272  snssiALTVD  45274  sstrALT2VD  45281  suctrALT2VD  45283  elex2VD  45285  elex22VD  45286  eqsbc2VD  45287  tpid3gVD  45289  en3lplem1VD  45290  en3lplem2VD  45291  3ornot23VD  45294  orbi1rVD  45295  19.21a3con13vVD  45299  exbirVD  45300  exbiriVD  45301  rspsbc2VD  45302  tratrbVD  45308  syl5impVD  45310  ssralv2VD  45313  imbi12VD  45320  imbi13VD  45321  sbcim2gVD  45322  sbcbiVD  45323  truniALTVD  45325  trintALTVD  45327  onfrALTlem3VD  45334  onfrALTlem2VD  45336  onfrALTlem1VD  45337  relopabVD  45348  19.41rgVD  45349  hbimpgVD  45351  ax6e2eqVD  45354  ax6e2ndeqVD  45356  sb5ALTVD  45360  vk15.4jVD  45361  con3ALTVD  45363