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

Theorem idn1 28342
Description: Virtual deduction identity rule which is id 19 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 19 . 2  |-  ( ph  ->  ph )
21dfvd1ir 28341 1  |-  (. ph  ->.  ph ).
Colors of variables: wff set class
Syntax hints:   (.wvd1 28337
This theorem is referenced by:  trsspwALT  28592  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  snssiALTVD  28602  snsslVD  28604  snelpwrVD  28606  unipwrVD  28608  sstrALT2VD  28610  suctrALT2VD  28612  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  zfregs2VD  28617  tpid3gVD  28618  en3lplem1VD  28619  en3lplem2VD  28620  en3lpVD  28621  3ornot23VD  28623  orbi1rVD  28624  3orbi123VD  28626  sbc3orgVD  28627  19.21a3con13vVD  28628  exbirVD  28629  exbiriVD  28630  rspsbc2VD  28631  3impexpVD  28632  3impexpbicomVD  28633  sbcoreleleqVD  28635  tratrbVD  28637  3ax5VD  28638  syl5impVD  28639  ssralv2VD  28642  ordelordALTVD  28643  equncomVD  28644  imbi12VD  28649  imbi13VD  28650  sbcim2gVD  28651  sbcbiVD  28652  trsbcVD  28653  truniALTVD  28654  trintALTVD  28656  undif3VD  28658  sbcssVD  28659  csbingVD  28660  onfrALTlem3VD  28663  simplbi2comgVD  28664  onfrALTlem2VD  28665  onfrALTVD  28667  csbeq2gVD  28668  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  con5VD  28676  relopabVD  28677  19.41rgVD  28678  2pm13.193VD  28679  hbimpgVD  28680  hbalgVD  28681  hbexgVD  28682  a9e2eqVD  28683  a9e2ndVD  28684  a9e2ndeqVD  28685  2sb5ndVD  28686  2uasbanhVD  28687  e2ebindVD  28688  sb5ALTVD  28689  vk15.4jVD  28690  notnot2ALTVD  28691  con3ALTVD  28692  sspwimpVD  28695  sspwimpcfVD  28697  suctrALTcfVD  28699
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 177  df-vd1 28338
  Copyright terms: Public domain W3C validator