Theorem idn2 45186

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

Syntax hints:  (   wvd2 45150

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 400  df-vd2 45151

This theorem is referenced by:  trsspwALT  45390  sspwtr  45393  pwtrVD  45396  pwtrrVD  45397  snssiALTVD  45399  sstrALT2VD  45406  suctrALT2VD  45408  elex2VD  45410  elex22VD  45411  eqsbc2VD  45412  tpid3gVD  45414  en3lplem1VD  45415  en3lplem2VD  45416  3ornot23VD  45419  orbi1rVD  45420  19.21a3con13vVD  45424  exbirVD  45425  exbiriVD  45426  rspsbc2VD  45427  tratrbVD  45433  syl5impVD  45435  ssralv2VD  45438  imbi12VD  45445  imbi13VD  45446  sbcim2gVD  45447  sbcbiVD  45448  truniALTVD  45450  trintALTVD  45452  onfrALTlem3VD  45459  onfrALTlem2VD  45461  onfrALTlem1VD  45462  relopabVD  45473  19.41rgVD  45474  hbimpgVD  45476  ax6e2eqVD  45479  ax6e2ndeqVD  45481  sb5ALTVD  45485  vk15.4jVD  45486  con3ALTVD  45488