Theorem idn2 33132

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

Syntax hints:   (.wvd2 33087

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 33088

This theorem is referenced by:  trsspwALT  33349  sspwtr  33352  pwtrVD  33357  pwtrrVD  33358  snssiALTVD  33360  sstrALT2VD  33367  suctrALT2VD  33369  elex2VD  33371  elex22VD  33372  eqsbc3rVD  33373  tpid3gVD  33375  en3lplem1VD  33376  en3lplem2VD  33377  3ornot23VD  33380  orbi1rVD  33381  19.21a3con13vVD  33385  exbirVD  33386  exbiriVD  33387  rspsbc2VD  33388  tratrbVD  33394  syl5impVD  33396  ssralv2VD  33399  imbi12VD  33406  imbi13VD  33407  sbcim2gVD  33408  sbcbiVD  33409  truniALTVD  33411  trintALTVD  33413  onfrALTlem3VD  33420  onfrALTlem2VD  33422  onfrALTlem1VD  33423  relopabVD  33434  19.41rgVD  33435  hbimpgVD  33437  ax6e2eqVD  33440  ax6e2ndeqVD  33442  sb5ALTVD  33446  vk15.4jVD  33447  con3ALTVD  33449