Theorem idn2 41847

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

Syntax hints:  (   wvd2 41811

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 210  df-an 400  df-vd2 41812

This theorem is referenced by:  trsspwALT  42052  sspwtr  42055  pwtrVD  42058  pwtrrVD  42059  snssiALTVD  42061  sstrALT2VD  42068  suctrALT2VD  42070  elex2VD  42072  elex22VD  42073  eqsbc3rVD  42074  tpid3gVD  42076  en3lplem1VD  42077  en3lplem2VD  42078  3ornot23VD  42081  orbi1rVD  42082  19.21a3con13vVD  42086  exbirVD  42087  exbiriVD  42088  rspsbc2VD  42089  tratrbVD  42095  syl5impVD  42097  ssralv2VD  42100  imbi12VD  42107  imbi13VD  42108  sbcim2gVD  42109  sbcbiVD  42110  truniALTVD  42112  trintALTVD  42114  onfrALTlem3VD  42121  onfrALTlem2VD  42123  onfrALTlem1VD  42124  relopabVD  42135  19.41rgVD  42136  hbimpgVD  42138  ax6e2eqVD  42141  ax6e2ndeqVD  42143  sb5ALTVD  42147  vk15.4jVD  42148  con3ALTVD  42150