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

Theorem idn1 30985
Description: Virtual deduction identity rule which is id 22 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 22 . 2  |-  ( ph  ->  ph )
21dfvd1ir 30984 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 30980
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-vd1 30981
This theorem is referenced by:  trsspwALT  31251  sspwtr  31254  pwtrVD  31259  pwtrrVD  31260  snssiALTVD  31262  snsslVD  31264  snelpwrVD  31266  unipwrVD  31267  sstrALT2VD  31269  suctrALT2VD  31271  elex2VD  31273  elex22VD  31274  eqsbc3rVD  31275  zfregs2VD  31276  tpid3gVD  31277  en3lplem1VD  31278  en3lplem2VD  31279  en3lpVD  31280  3ornot23VD  31282  orbi1rVD  31283  3orbi123VD  31285  sbc3orgVD  31286  19.21a3con13vVD  31287  exbirVD  31288  exbiriVD  31289  rspsbc2VD  31290  3impexpVD  31291  3impexpbicomVD  31292  sbcoreleleqVD  31294  tratrbVD  31296  3ax4VD  31297  syl5impVD  31298  ssralv2VD  31301  ordelordALTVD  31302  equncomVD  31303  imbi12VD  31308  imbi13VD  31309  sbcim2gVD  31310  sbcbiVD  31311  trsbcVD  31312  truniALTVD  31313  trintALTVD  31315  undif3VD  31317  sbcssgVD  31318  csbingVD  31319  onfrALTlem3VD  31322  simplbi2comgVD  31323  onfrALTlem2VD  31324  onfrALTVD  31326  csbeq2gVD  31327  csbsngVD  31328  csbxpgVD  31329  csbresgVD  31330  csbrngVD  31331  csbima12gALTVD  31332  csbunigVD  31333  csbfv12gALTVD  31334  con5VD  31335  relopabVD  31336  19.41rgVD  31337  2pm13.193VD  31338  hbimpgVD  31339  hbalgVD  31340  hbexgVD  31341  ax6e2eqVD  31342  ax6e2ndVD  31343  ax6e2ndeqVD  31344  2sb5ndVD  31345  2uasbanhVD  31346  e2ebindVD  31347  sb5ALTVD  31348  vk15.4jVD  31349  notnot2ALTVD  31350  con3ALTVD  31351  sspwimpVD  31354  sspwimpcfVD  31356  suctrALTcfVD  31358
  Copyright terms: Public domain W3C validator