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

Theorem idn2 28615
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 28579 1  |-  (. ph ,. ps  ->.  ps ).
Colors of variables: wff set class
Syntax hints:   (.wvd2 28570
This theorem is referenced by:  trsspwALT  28832  sspwtr  28835  pwtrVD  28838  pwtrrVD  28839  snssiALTVD  28840  sstrALT2VD  28847  suctrALT2VD  28849  elex2VD  28851  elex22VD  28852  eqsbc3rVD  28853  tpid3gVD  28855  en3lplem1VD  28856  en3lplem2VD  28857  3ornot23VD  28860  orbi1rVD  28861  19.21a3con13vVD  28865  exbirVD  28866  exbiriVD  28867  rspsbc2VD  28868  tratrbVD  28874  syl5impVD  28876  ssralv2VD  28879  imbi12VD  28886  imbi13VD  28887  sbcim2gVD  28888  sbcbiVD  28889  truniALTVD  28891  trintALTVD  28893  onfrALTlem3VD  28900  onfrALTlem2VD  28902  onfrALTlem1VD  28903  relopabVD  28914  19.41rgVD  28915  hbimpgVD  28917  a9e2eqVD  28920  a9e2ndeqVD  28922  sb5ALTVD  28926  vk15.4jVD  28927  con3ALTVD  28929
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 28571
  Copyright terms: Public domain W3C validator