Theorem idn2 40953

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

Syntax hints:  (   wvd2 40917

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 209  df-an 399  df-vd2 40918

This theorem is referenced by:  trsspwALT  41158  sspwtr  41161  pwtrVD  41164  pwtrrVD  41165  snssiALTVD  41167  sstrALT2VD  41174  suctrALT2VD  41176  elex2VD  41178  elex22VD  41179  eqsbc3rVD  41180  tpid3gVD  41182  en3lplem1VD  41183  en3lplem2VD  41184  3ornot23VD  41187  orbi1rVD  41188  19.21a3con13vVD  41192  exbirVD  41193  exbiriVD  41194  rspsbc2VD  41195  tratrbVD  41201  syl5impVD  41203  ssralv2VD  41206  imbi12VD  41213  imbi13VD  41214  sbcim2gVD  41215  sbcbiVD  41216  truniALTVD  41218  trintALTVD  41220  onfrALTlem3VD  41227  onfrALTlem2VD  41229  onfrALTlem1VD  41230  relopabVD  41241  19.41rgVD  41242  hbimpgVD  41244  ax6e2eqVD  41247  ax6e2ndeqVD  41249  sb5ALTVD  41253  vk15.4jVD  41254  con3ALTVD  41256