Theorem idn2 44716

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

Syntax hints:  (   wvd2 44680

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 44681

This theorem is referenced by:  trsspwALT  44920  sspwtr  44923  pwtrVD  44926  pwtrrVD  44927  snssiALTVD  44929  sstrALT2VD  44936  suctrALT2VD  44938  elex2VD  44940  elex22VD  44941  eqsbc2VD  44942  tpid3gVD  44944  en3lplem1VD  44945  en3lplem2VD  44946  3ornot23VD  44949  orbi1rVD  44950  19.21a3con13vVD  44954  exbirVD  44955  exbiriVD  44956  rspsbc2VD  44957  tratrbVD  44963  syl5impVD  44965  ssralv2VD  44968  imbi12VD  44975  imbi13VD  44976  sbcim2gVD  44977  sbcbiVD  44978  truniALTVD  44980  trintALTVD  44982  onfrALTlem3VD  44989  onfrALTlem2VD  44991  onfrALTlem1VD  44992  relopabVD  45003  19.41rgVD  45004  hbimpgVD  45006  ax6e2eqVD  45009  ax6e2ndeqVD  45011  sb5ALTVD  45015  vk15.4jVD  45016  con3ALTVD  45018