Theorem idn2 31638

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

Syntax hints:   (.wvd2 31593

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 371  df-vd2 31594

This theorem is referenced by:  trsspwALT  31855  sspwtr  31858  pwtrVD  31863  pwtrrVD  31864  snssiALTVD  31866  sstrALT2VD  31873  suctrALT2VD  31875  elex2VD  31877  elex22VD  31878  eqsbc3rVD  31879  tpid3gVD  31881  en3lplem1VD  31882  en3lplem2VD  31883  3ornot23VD  31886  orbi1rVD  31887  19.21a3con13vVD  31891  exbirVD  31892  exbiriVD  31893  rspsbc2VD  31894  tratrbVD  31900  syl5impVD  31902  ssralv2VD  31905  imbi12VD  31912  imbi13VD  31913  sbcim2gVD  31914  sbcbiVD  31915  truniALTVD  31917  trintALTVD  31919  onfrALTlem3VD  31926  onfrALTlem2VD  31928  onfrALTlem1VD  31929  relopabVD  31940  19.41rgVD  31941  hbimpgVD  31943  ax6e2eqVD  31946  ax6e2ndeqVD  31948  sb5ALTVD  31952  vk15.4jVD  31953  con3ALTVD  31955