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

Theorem idn1 36582
Description: Virtual deduction identity rule which is id 23 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 23 . 2  |-  ( ph  ->  ph )
21dfvd1ir 36581 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 36577
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 188  df-vd1 36578
This theorem is referenced by:  trsspwALT  36846  sspwtr  36849  pwtrVD  36860  pwtrrVD  36861  snssiALTVD  36863  snsslVD  36865  snelpwrVD  36867  unipwrVD  36868  sstrALT2VD  36870  suctrALT2VD  36872  elex2VD  36874  elex22VD  36875  eqsbc3rVD  36876  zfregs2VD  36877  tpid3gVD  36878  en3lplem1VD  36879  en3lplem2VD  36880  en3lpVD  36881  3ornot23VD  36883  orbi1rVD  36884  3orbi123VD  36886  sbc3orgVD  36887  19.21a3con13vVD  36888  exbirVD  36889  exbiriVD  36890  rspsbc2VD  36891  3impexpVD  36892  3impexpbicomVD  36893  sbcoreleleqVD  36896  tratrbVD  36898  al2imVD  36899  syl5impVD  36900  ssralv2VD  36903  ordelordALTVD  36904  equncomVD  36905  imbi12VD  36910  imbi13VD  36911  sbcim2gVD  36912  sbcbiVD  36913  trsbcVD  36914  truniALTVD  36915  trintALTVD  36917  undif3VD  36919  sbcssgVD  36920  csbingVD  36921  onfrALTlem3VD  36924  simplbi2comtVD  36925  onfrALTlem2VD  36926  onfrALTVD  36928  csbeq2gVD  36929  csbsngVD  36930  csbxpgVD  36931  csbresgVD  36932  csbrngVD  36933  csbima12gALTVD  36934  csbunigVD  36935  csbfv12gALTVD  36936  con5VD  36937  relopabVD  36938  19.41rgVD  36939  2pm13.193VD  36940  hbimpgVD  36941  hbalgVD  36942  hbexgVD  36943  ax6e2eqVD  36944  ax6e2ndVD  36945  ax6e2ndeqVD  36946  2sb5ndVD  36947  2uasbanhVD  36948  e2ebindVD  36949  sb5ALTVD  36950  vk15.4jVD  36951  notnot2ALTVD  36952  con3ALTVD  36953  sspwimpVD  36956  sspwimpcfVD  36958  suctrALTcfVD  36960
  Copyright terms: Public domain W3C validator