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

Theorem idn2 33793
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 33757 1  |-  (. ph ,. ps  ->.  ps ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd2 33748
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 369  df-vd2 33749
This theorem is referenced by:  trsspwALT  34010  sspwtr  34013  pwtrVD  34024  pwtrrVD  34025  snssiALTVD  34027  sstrALT2VD  34034  suctrALT2VD  34036  elex2VD  34038  elex22VD  34039  eqsbc3rVD  34040  tpid3gVD  34042  en3lplem1VD  34043  en3lplem2VD  34044  3ornot23VD  34047  orbi1rVD  34048  19.21a3con13vVD  34052  exbirVD  34053  exbiriVD  34054  rspsbc2VD  34055  tratrbVD  34062  syl5impVD  34064  ssralv2VD  34067  imbi12VD  34074  imbi13VD  34075  sbcim2gVD  34076  sbcbiVD  34077  truniALTVD  34079  trintALTVD  34081  onfrALTlem3VD  34088  onfrALTlem2VD  34090  onfrALTlem1VD  34091  relopabVD  34102  19.41rgVD  34103  hbimpgVD  34105  ax6e2eqVD  34108  ax6e2ndeqVD  34110  sb5ALTVD  34114  vk15.4jVD  34115  con3ALTVD  34117
  Copyright terms: Public domain W3C validator