Theorem idn2 37034

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

Proof of Theorem idn2

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

Syntax hints:   (.wvd2 36989

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 190  df-an 377  df-vd2 36990

This theorem is referenced by:  trsspwALT  37245  sspwtr  37248  pwtrVD  37259  pwtrrVD  37260  snssiALTVD  37262  sstrALT2VD  37269  suctrALT2VD  37271  elex2VD  37273  elex22VD  37274  eqsbc3rVD  37275  tpid3gVD  37277  en3lplem1VD  37278  en3lplem2VD  37279  3ornot23VD  37282  orbi1rVD  37283  19.21a3con13vVD  37287  exbirVD  37288  exbiriVD  37289  rspsbc2VD  37290  tratrbVD  37297  syl5impVD  37299  ssralv2VD  37302  imbi12VD  37309  imbi13VD  37310  sbcim2gVD  37311  sbcbiVD  37312  truniALTVD  37314  trintALTVD  37316  onfrALTlem3VD  37323  onfrALTlem2VD  37325  onfrALTlem1VD  37326  relopabVD  37337  19.41rgVD  37338  hbimpgVD  37340  ax6e2eqVD  37343  ax6e2ndeqVD  37345  sb5ALTVD  37349  vk15.4jVD  37350  con3ALTVD  37352