Theorem idn2 44969

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

Syntax hints:  (   wvd2 44933

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 44934

This theorem is referenced by:  trsspwALT  45173  sspwtr  45176  pwtrVD  45179  pwtrrVD  45180  snssiALTVD  45182  sstrALT2VD  45189  suctrALT2VD  45191  elex2VD  45193  elex22VD  45194  eqsbc2VD  45195  tpid3gVD  45197  en3lplem1VD  45198  en3lplem2VD  45199  3ornot23VD  45202  orbi1rVD  45203  19.21a3con13vVD  45207  exbirVD  45208  exbiriVD  45209  rspsbc2VD  45210  tratrbVD  45216  syl5impVD  45218  ssralv2VD  45221  imbi12VD  45228  imbi13VD  45229  sbcim2gVD  45230  sbcbiVD  45231  truniALTVD  45233  trintALTVD  45235  onfrALTlem3VD  45242  onfrALTlem2VD  45244  onfrALTlem1VD  45245  relopabVD  45256  19.41rgVD  45257  hbimpgVD  45259  ax6e2eqVD  45262  ax6e2ndeqVD  45264  sb5ALTVD  45268  vk15.4jVD  45269  con3ALTVD  45271