Theorem idn2 44638

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

Syntax hints:  (   wvd2 44602

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 44603

This theorem is referenced by:  trsspwALT  44842  sspwtr  44845  pwtrVD  44848  pwtrrVD  44849  snssiALTVD  44851  sstrALT2VD  44858  suctrALT2VD  44860  elex2VD  44862  elex22VD  44863  eqsbc2VD  44864  tpid3gVD  44866  en3lplem1VD  44867  en3lplem2VD  44868  3ornot23VD  44871  orbi1rVD  44872  19.21a3con13vVD  44876  exbirVD  44877  exbiriVD  44878  rspsbc2VD  44879  tratrbVD  44885  syl5impVD  44887  ssralv2VD  44890  imbi12VD  44897  imbi13VD  44898  sbcim2gVD  44899  sbcbiVD  44900  truniALTVD  44902  trintALTVD  44904  onfrALTlem3VD  44911  onfrALTlem2VD  44913  onfrALTlem1VD  44914  relopabVD  44925  19.41rgVD  44926  hbimpgVD  44928  ax6e2eqVD  44931  ax6e2ndeqVD  44933  sb5ALTVD  44937  vk15.4jVD  44938  con3ALTVD  44940