Theorem idn2 44576

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

Syntax hints:  (   wvd2 44540

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 44541

This theorem is referenced by:  trsspwALT  44780  sspwtr  44783  pwtrVD  44786  pwtrrVD  44787  snssiALTVD  44789  sstrALT2VD  44796  suctrALT2VD  44798  elex2VD  44800  elex22VD  44801  eqsbc2VD  44802  tpid3gVD  44804  en3lplem1VD  44805  en3lplem2VD  44806  3ornot23VD  44809  orbi1rVD  44810  19.21a3con13vVD  44814  exbirVD  44815  exbiriVD  44816  rspsbc2VD  44817  tratrbVD  44823  syl5impVD  44825  ssralv2VD  44828  imbi12VD  44835  imbi13VD  44836  sbcim2gVD  44837  sbcbiVD  44838  truniALTVD  44840  trintALTVD  44842  onfrALTlem3VD  44849  onfrALTlem2VD  44851  onfrALTlem1VD  44852  relopabVD  44863  19.41rgVD  44864  hbimpgVD  44866  ax6e2eqVD  44869  ax6e2ndeqVD  44871  sb5ALTVD  44875  vk15.4jVD  44876  con3ALTVD  44878