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

Theorem idn1 28374
Description: Virtual deduction identity rule which is id 20 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 20 . 2  |-  ( ph  ->  ph )
21dfvd1ir 28373 1  |-  (. ph  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28369
This theorem is referenced by:  trsspwALT  28640  sspwtr  28643  pwtrVD  28646  pwtrrVD  28647  snssiALTVD  28648  snsslVD  28650  snelpwrVD  28652  unipwrVD  28653  sstrALT2VD  28655  suctrALT2VD  28657  elex2VD  28659  elex22VD  28660  eqsbc3rVD  28661  zfregs2VD  28662  tpid3gVD  28663  en3lplem1VD  28664  en3lplem2VD  28665  en3lpVD  28666  3ornot23VD  28668  orbi1rVD  28669  3orbi123VD  28671  sbc3orgVD  28672  19.21a3con13vVD  28673  exbirVD  28674  exbiriVD  28675  rspsbc2VD  28676  3impexpVD  28677  3impexpbicomVD  28678  sbcoreleleqVD  28680  tratrbVD  28682  3ax5VD  28683  syl5impVD  28684  ssralv2VD  28687  ordelordALTVD  28688  equncomVD  28689  imbi12VD  28694  imbi13VD  28695  sbcim2gVD  28696  sbcbiVD  28697  trsbcVD  28698  truniALTVD  28699  trintALTVD  28701  undif3VD  28703  sbcssVD  28704  csbingVD  28705  onfrALTlem3VD  28708  simplbi2comgVD  28709  onfrALTlem2VD  28710  onfrALTVD  28712  csbeq2gVD  28713  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbima12gALTVD  28718  csbunigVD  28719  csbfv12gALTVD  28720  con5VD  28721  relopabVD  28722  19.41rgVD  28723  2pm13.193VD  28724  hbimpgVD  28725  hbalgVD  28726  hbexgVD  28727  a9e2eqVD  28728  a9e2ndVD  28729  a9e2ndeqVD  28730  2sb5ndVD  28731  2uasbanhVD  28732  e2ebindVD  28733  sb5ALTVD  28734  vk15.4jVD  28735  notnot2ALTVD  28736  con3ALTVD  28737  sspwimpVD  28740  sspwimpcfVD  28742  suctrALTcfVD  28744
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-vd1 28370
  Copyright terms: Public domain W3C validator