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

Theorem idn2 31638
Description: Virtual deduction identity rule which is idd 24 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 24 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
21dfvd2ir 31602 1  |-  (. ph ,. ps  ->.  ps ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd2 31593
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 185  df-an 371  df-vd2 31594
This theorem is referenced by:  trsspwALT  31855  sspwtr  31858  pwtrVD  31863  pwtrrVD  31864  snssiALTVD  31866  sstrALT2VD  31873  suctrALT2VD  31875  elex2VD  31877  elex22VD  31878  eqsbc3rVD  31879  tpid3gVD  31881  en3lplem1VD  31882  en3lplem2VD  31883  3ornot23VD  31886  orbi1rVD  31887  19.21a3con13vVD  31891  exbirVD  31892  exbiriVD  31893  rspsbc2VD  31894  tratrbVD  31900  syl5impVD  31902  ssralv2VD  31905  imbi12VD  31912  imbi13VD  31913  sbcim2gVD  31914  sbcbiVD  31915  truniALTVD  31917  trintALTVD  31919  onfrALTlem3VD  31926  onfrALTlem2VD  31928  onfrALTlem1VD  31929  relopabVD  31940  19.41rgVD  31941  hbimpgVD  31943  ax6e2eqVD  31946  ax6e2ndeqVD  31948  sb5ALTVD  31952  vk15.4jVD  31953  con3ALTVD  31955
  Copyright terms: Public domain W3C validator