Theorem idn2 45856

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

This proof depends on syntax axioms:  (   wvd2 45820

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 45821

This theorem is used by:  trsspwALT  46060  sspwtr  46063  pwtrVD  46066  pwtrrVD  46067  snssiALTVD  46069  sstrALT2VD  46076  suctrALT2VD  46078  elex2VD  46080  elex22VD  46081  eqsbc2VD  46082  tpid3gVD  46084  en3lplem1VD  46085  en3lplem2VD  46086  3ornot23VD  46089  orbi1rVD  46090  19.21a3con13vVD  46094  exbirVD  46095  exbiriVD  46096  rspsbc2VD  46097  tratrbVD  46103  syl5impVD  46105  ssralv2VD  46108  imbi12VD  46115  imbi13VD  46116  sbcim2gVD  46117  sbcbiVD  46118  truniALTVD  46120  trintALTVD  46122  onfrALTlem3VD  46129  onfrALTlem2VD  46131  onfrALTlem1VD  46132  relopabVD  46143  19.41rgVD  46144  hbimpgVD  46146  ax6e2eqVD  46149  ax6e2ndeqVD  46151  sb5ALTVD  46155  vk15.4jVD  46156  con3ALTVD  46158