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

Theorem idn1 28727
Description: Virtual deduction identity rule which is id 21 with virtual deduction symbols. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
idn1  |-  (. ph  ->.  ph ).

Proof of Theorem idn1
StepHypRef Expression
1 id 21 . 2  |-  ( ph  ->  ph )
21dfvd1ir 28726 1  |-  (. ph  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28722
This theorem is referenced by:  trsspwALT  28993  sspwtr  28996  pwtrVD  28999  pwtrrVD  29000  snssiALTVD  29001  snsslVD  29003  snelpwrVD  29005  unipwrVD  29006  sstrALT2VD  29008  suctrALT2VD  29010  elex2VD  29012  elex22VD  29013  eqsbc3rVD  29014  zfregs2VD  29015  tpid3gVD  29016  en3lplem1VD  29017  en3lplem2VD  29018  en3lpVD  29019  3ornot23VD  29021  orbi1rVD  29022  3orbi123VD  29024  sbc3orgVD  29025  19.21a3con13vVD  29026  exbirVD  29027  exbiriVD  29028  rspsbc2VD  29029  3impexpVD  29030  3impexpbicomVD  29031  sbcoreleleqVD  29033  tratrbVD  29035  3ax5VD  29036  syl5impVD  29037  ssralv2VD  29040  ordelordALTVD  29041  equncomVD  29042  imbi12VD  29047  imbi13VD  29048  sbcim2gVD  29049  sbcbiVD  29050  trsbcVD  29051  truniALTVD  29052  trintALTVD  29054  undif3VD  29056  sbcssVD  29057  csbingVD  29058  onfrALTlem3VD  29061  simplbi2comgVD  29062  onfrALTlem2VD  29063  onfrALTVD  29065  csbeq2gVD  29066  csbsngVD  29067  csbxpgVD  29068  csbresgVD  29069  csbrngVD  29070  csbima12gALTVD  29071  csbunigVD  29072  csbfv12gALTVD  29073  con5VD  29074  relopabVD  29075  19.41rgVD  29076  2pm13.193VD  29077  hbimpgVD  29078  hbalgVD  29079  hbexgVD  29080  a9e2eqVD  29081  a9e2ndVD  29082  a9e2ndeqVD  29083  2sb5ndVD  29084  2uasbanhVD  29085  e2ebindVD  29086  sb5ALTVD  29087  vk15.4jVD  29088  notnot2ALTVD  29089  con3ALTVD  29090  sspwimpVD  29093  sspwimpcfVD  29095  suctrALTcfVD  29097
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 179  df-vd1 28723
  Copyright terms: Public domain W3C validator