Theorem idn2 42604

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

Syntax hints:  (   wvd2 42568

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 206  df-an 398  df-vd2 42569

This theorem is referenced by:  trsspwALT  42809  sspwtr  42812  pwtrVD  42815  pwtrrVD  42816  snssiALTVD  42818  sstrALT2VD  42825  suctrALT2VD  42827  elex2VD  42829  elex22VD  42830  eqsbc2VD  42831  tpid3gVD  42833  en3lplem1VD  42834  en3lplem2VD  42835  3ornot23VD  42838  orbi1rVD  42839  19.21a3con13vVD  42843  exbirVD  42844  exbiriVD  42845  rspsbc2VD  42846  tratrbVD  42852  syl5impVD  42854  ssralv2VD  42857  imbi12VD  42864  imbi13VD  42865  sbcim2gVD  42866  sbcbiVD  42867  truniALTVD  42869  trintALTVD  42871  onfrALTlem3VD  42878  onfrALTlem2VD  42880  onfrALTlem1VD  42881  relopabVD  42892  19.41rgVD  42893  hbimpgVD  42895  ax6e2eqVD  42898  ax6e2ndeqVD  42900  sb5ALTVD  42904  vk15.4jVD  42905  con3ALTVD  42907