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

Theorem idn2 28056
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
StepHypRef Expression
1 idd 22 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
21dfvd2ir 28020 1  |-  (. ph ,. ps  ->.  ps ).
Colors of variables: wff set class
Syntax hints:   (.wvd2 28011
This theorem is referenced by:  trsspwALT  28273  sspwtr  28276  pwtrVD  28279  pwtrrVD  28280  snssiALTVD  28281  sstrALT2VD  28288  suctrALT2VD  28290  elex2VD  28292  elex22VD  28293  eqsbc3rVD  28294  tpid3gVD  28296  en3lplem1VD  28297  en3lplem2VD  28298  3ornot23VD  28301  orbi1rVD  28302  19.21a3con13vVD  28306  exbirVD  28307  exbiriVD  28308  rspsbc2VD  28309  tratrbVD  28315  syl5impVD  28317  ssralv2VD  28320  imbi12VD  28327  imbi13VD  28328  sbcim2gVD  28329  sbcbiVD  28330  truniALTVD  28332  trintALTVD  28334  onfrALTlem3VD  28341  onfrALTlem2VD  28343  onfrALTlem1VD  28344  relopabVD  28355  19.41rgVD  28356  hbimpgVD  28358  a9e2eqVD  28361  a9e2ndeqVD  28363  sb5ALTVD  28367  vk15.4jVD  28368  con3ALTVD  28370
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 28012
  Copyright terms: Public domain W3C validator