Theorem idn2 37859

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

Syntax hints:  (   wvd2 37814

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 196  df-an 385  df-vd2 37815

This theorem is referenced by:  trsspwALT  38067  sspwtr  38070  pwtrVD  38081  pwtrrVD  38082  snssiALTVD  38084  sstrALT2VD  38091  suctrALT2VD  38093  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  tpid3gVD  38099  en3lplem1VD  38100  en3lplem2VD  38101  3ornot23VD  38104  orbi1rVD  38105  19.21a3con13vVD  38109  exbirVD  38110  exbiriVD  38111  rspsbc2VD  38112  tratrbVD  38119  syl5impVD  38121  ssralv2VD  38124  imbi12VD  38131  imbi13VD  38132  sbcim2gVD  38133  sbcbiVD  38134  truniALTVD  38136  trintALTVD  38138  onfrALTlem3VD  38145  onfrALTlem2VD  38147  onfrALTlem1VD  38148  relopabVD  38159  19.41rgVD  38160  hbimpgVD  38162  ax6e2eqVD  38165  ax6e2ndeqVD  38167  sb5ALTVD  38171  vk15.4jVD  38172  con3ALTVD  38174