Theorem idn2 28423

Description: Virtual deduction identity rule which is idd 22 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 22	. 2 |- ( ph -> ( ps -> ps ) )
2	1	dfvd2ir 28387	1 |- (. ph ,. ps ->. ps ).

Syntax hints:   (.wvd2 28378

This theorem is referenced by:  trsspwALT  28640  sspwtr  28643  pwtrVD  28646  pwtrrVD  28647  snssiALTVD  28648  sstrALT2VD  28655  suctrALT2VD  28657  elex2VD  28659  elex22VD  28660  eqsbc3rVD  28661  tpid3gVD  28663  en3lplem1VD  28664  en3lplem2VD  28665  3ornot23VD  28668  orbi1rVD  28669  19.21a3con13vVD  28673  exbirVD  28674  exbiriVD  28675  rspsbc2VD  28676  tratrbVD  28682  syl5impVD  28684  ssralv2VD  28687  imbi12VD  28694  imbi13VD  28695  sbcim2gVD  28696  sbcbiVD  28697  truniALTVD  28699  trintALTVD  28701  onfrALTlem3VD  28708  onfrALTlem2VD  28710  onfrALTlem1VD  28711  relopabVD  28722  19.41rgVD  28723  hbimpgVD  28725  a9e2eqVD  28728  a9e2ndeqVD  28730  sb5ALTVD  28734  vk15.4jVD  28735  con3ALTVD  28737

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-vd2 28379