Theorem idn2 44587

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

Syntax hints:  (   wvd2 44551

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 44552

This theorem is referenced by:  trsspwALT  44791  sspwtr  44794  pwtrVD  44797  pwtrrVD  44798  snssiALTVD  44800  sstrALT2VD  44807  suctrALT2VD  44809  elex2VD  44811  elex22VD  44812  eqsbc2VD  44813  tpid3gVD  44815  en3lplem1VD  44816  en3lplem2VD  44817  3ornot23VD  44820  orbi1rVD  44821  19.21a3con13vVD  44825  exbirVD  44826  exbiriVD  44827  rspsbc2VD  44828  tratrbVD  44834  syl5impVD  44836  ssralv2VD  44839  imbi12VD  44846  imbi13VD  44847  sbcim2gVD  44848  sbcbiVD  44849  truniALTVD  44851  trintALTVD  44853  onfrALTlem3VD  44860  onfrALTlem2VD  44862  onfrALTlem1VD  44863  relopabVD  44874  19.41rgVD  44875  hbimpgVD  44877  ax6e2eqVD  44880  ax6e2ndeqVD  44882  sb5ALTVD  44886  vk15.4jVD  44887  con3ALTVD  44889