Theorem idn2 33793

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	|- (. ph ,. ps ->. ps ).

Proof of Theorem idn2

Step	Hyp	Ref	Expression
1		idd 24	. 2 |- ( ph -> ( ps -> ps ) )
2	1	dfvd2ir 33757	1 |- (. ph ,. ps ->. ps ).

Syntax hints:   (.wvd2 33748

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 185  df-an 369  df-vd2 33749

This theorem is referenced by:  trsspwALT  34010  sspwtr  34013  pwtrVD  34024  pwtrrVD  34025  snssiALTVD  34027  sstrALT2VD  34034  suctrALT2VD  34036  elex2VD  34038  elex22VD  34039  eqsbc3rVD  34040  tpid3gVD  34042  en3lplem1VD  34043  en3lplem2VD  34044  3ornot23VD  34047  orbi1rVD  34048  19.21a3con13vVD  34052  exbirVD  34053  exbiriVD  34054  rspsbc2VD  34055  tratrbVD  34062  syl5impVD  34064  ssralv2VD  34067  imbi12VD  34074  imbi13VD  34075  sbcim2gVD  34076  sbcbiVD  34077  truniALTVD  34079  trintALTVD  34081  onfrALTlem3VD  34088  onfrALTlem2VD  34090  onfrALTlem1VD  34091  relopabVD  34102  19.41rgVD  34103  hbimpgVD  34105  ax6e2eqVD  34108  ax6e2ndeqVD  34110  sb5ALTVD  34114  vk15.4jVD  34115  con3ALTVD  34117