Theorem idn2 32354

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

Syntax hints:   (.wvd2 32309

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 32310

This theorem is referenced by:  trsspwALT  32571  sspwtr  32574  pwtrVD  32579  pwtrrVD  32580  snssiALTVD  32582  sstrALT2VD  32589  suctrALT2VD  32591  elex2VD  32593  elex22VD  32594  eqsbc3rVD  32595  tpid3gVD  32597  en3lplem1VD  32598  en3lplem2VD  32599  3ornot23VD  32602  orbi1rVD  32603  19.21a3con13vVD  32607  exbirVD  32608  exbiriVD  32609  rspsbc2VD  32610  tratrbVD  32616  syl5impVD  32618  ssralv2VD  32621  imbi12VD  32628  imbi13VD  32629  sbcim2gVD  32630  sbcbiVD  32631  truniALTVD  32633  trintALTVD  32635  onfrALTlem3VD  32642  onfrALTlem2VD  32644  onfrALTlem1VD  32645  relopabVD  32656  19.41rgVD  32657  hbimpgVD  32659  ax6e2eqVD  32662  ax6e2ndeqVD  32664  sb5ALTVD  32668  vk15.4jVD  32669  con3ALTVD  32671