Theorem idn2 45436

Description: Virtual deduction identity rule which is idd 25 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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
2	1	dfvd2ir 45409	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )

This proof depends on syntax axioms:  (   wvd2 45400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd2 45401

This theorem is used by:  trsspwALT  45640  sspwtr  45643  pwtrVD  45646  pwtrrVD  45647  snssiALTVD  45649  sstrALT2VD  45656  suctrALT2VD  45658  elex2VD  45660  elex22VD  45661  eqsbc2VD  45662  tpid3gVD  45664  en3lplem1VD  45665  en3lplem2VD  45666  3ornot23VD  45669  orbi1rVD  45670  19.21a3con13vVD  45674  exbirVD  45675  exbiriVD  45676  rspsbc2VD  45677  tratrbVD  45683  syl5impVD  45685  ssralv2VD  45688  imbi12VD  45695  imbi13VD  45696  sbcim2gVD  45697  sbcbiVD  45698  truniALTVD  45700  trintALTVD  45702  onfrALTlem3VD  45709  onfrALTlem2VD  45711  onfrALTlem1VD  45712  relopabVD  45723  19.41rgVD  45724  hbimpgVD  45726  ax6e2eqVD  45729  ax6e2ndeqVD  45731  sb5ALTVD  45735  vk15.4jVD  45736  con3ALTVD  45738