Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  idn2 Unicode version

Theorem idn2 28690
Description: Virtual deduction identity rule which is idd 21 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
StepHypRef Expression
1 idd 21 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
21dfvd2ir 28654 1  |-  (. ph ,. ps  ->.  ps ).
Colors of variables: wff set class
Syntax hints:   (.wvd2 28645
This theorem is referenced by:  trsspwALT  28908  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  snssiALTVD  28918  sstrALT2VD  28926  suctrALT2VD  28928  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  tpid3gVD  28934  en3lplem1VD  28935  en3lplem2VD  28936  3ornot23VD  28939  orbi1rVD  28940  19.21a3con13vVD  28944  exbirVD  28945  exbiriVD  28946  rspsbc2VD  28947  tratrbVD  28953  syl5impVD  28955  ssralv2VD  28958  imbi12VD  28965  imbi13VD  28966  sbcim2gVD  28967  sbcbiVD  28968  truniALTVD  28970  trintALTVD  28972  onfrALTlem3VD  28979  onfrALTlem2VD  28981  onfrALTlem1VD  28982  relopabVD  28993  19.41rgVD  28994  hbimpgVD  28996  a9e2eqVD  28999  a9e2ndeqVD  29001  sb5ALTVD  29005  vk15.4jVD  29006  con3ALTVD  29008
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 177  df-an 360  df-vd2 28646
  Copyright terms: Public domain W3C validator