Theorem idn2 45213

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

Syntax hints:  (   wvd2 45177

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 210  df-an 401  df-vd2 45178

This theorem is referenced by:  trsspwALT  45417  sspwtr  45420  pwtrVD  45423  pwtrrVD  45424  snssiALTVD  45426  sstrALT2VD  45433  suctrALT2VD  45435  elex2VD  45437  elex22VD  45438  eqsbc2VD  45439  tpid3gVD  45441  en3lplem1VD  45442  en3lplem2VD  45443  3ornot23VD  45446  orbi1rVD  45447  19.21a3con13vVD  45451  exbirVD  45452  exbiriVD  45453  rspsbc2VD  45454  tratrbVD  45460  syl5impVD  45462  ssralv2VD  45465  imbi12VD  45472  imbi13VD  45473  sbcim2gVD  45474  sbcbiVD  45475  truniALTVD  45477  trintALTVD  45479  onfrALTlem3VD  45486  onfrALTlem2VD  45488  onfrALTlem1VD  45489  relopabVD  45500  19.41rgVD  45501  hbimpgVD  45503  ax6e2eqVD  45506  ax6e2ndeqVD  45508  sb5ALTVD  45512  vk15.4jVD  45513  con3ALTVD  45515