ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  id GIF version

Theorem id 19
Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Assertion
Ref Expression
id (𝜑𝜑)

Proof of Theorem id
StepHypRef Expression
1 ax-1 5 . 2 (𝜑 → (𝜑𝜑))
2 ax-1 5 . 2 (𝜑 → ((𝜑𝜑) → 𝜑))
31, 2mpd 13 1 (𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  39  pm2.43i  48  pm2.43d  49  pm2.43a  50  imim2  54  imim1i  59  imim1  75  pm2.04  81  pm2.86  99  biimprd  156  biimpcd  157  biimprcd  158  biid  169  bibi2i  225  imbi1  234  imbi2  235  bibi1  238  pm3.3  257  pm3.31  258  jctl  307  jctr  308  ancli  316  ancri  317  anc2li  322  anc2ri  323  anim12i  331  anim1i  333  anim2i  334  pm4.24  387  anass  393  mpdan  412  mpancom  413  pm5.32  441  anbi1  454  anbi2  455  mpan10  458  simpll  496  simplr  497  simprl  498  simprr  499  pm3.45  562  pm5.36  575  con2i  590  notnot  592  con3i  595  biijust  603  con3  604  con2  605  notbii  627  pm5.19  655  olc  665  orc  666  pm2.621  699  pm1.2  706  orim1i  710  orim2i  711  pm2.41  726  pm2.42  727  pm2.4  728  pm4.44  729  orim2  736  orbi1  739  pm2.38  750  pm2.74  754  pm3.2ni  760  pm4.79dc  845  biantr  896  3anim1i  1127  3anim2i  1128  3anim3i  1129  mpd3an23  1273  trujust  1289  tru  1291  dftru2  1295  truimtru  1343  falimfal  1346  3impexp  1369  19.26  1413  19.8a  1525  19.9ht  1575  ax6blem  1583  19.36i  1605  19.41h  1618  equsb1  1712  sbieh  1717  dveeq2or  1741  spsbim  1768  2ax17  1803  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  moanmo  2022  nfcvf  2246  neqne  2259  neneq  2273  necon3i  2299  nebidc  2331  vtoclgft  2663  eueq2dc  2779  cdeqcv  2823  ru  2828  sbcied2  2865  sbcralt  2904  sbcrext  2905  csbiebt  2956  csbied2  2964  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  ssid  3033  difss2  3117  ddifstab  3121  abvor0dc  3295  ssdifeq0  3352  ifbi  3397  rabsnt  3502  unisng  3655  dfnfc2  3656  a9evsep  3938  axnul  3941  intid  4027  opm  4037  opth1  4039  opth  4040  copsex4g  4050  0nelop  4051  moop2  4054  pocl  4106  swopo  4109  limeq  4180  suceq  4205  eusvnfb  4252  onintexmid  4363  nn0eln0  4408  elvvuni  4472  coss1  4561  coss2  4562  dmxpm  4626  elrnmpt1  4656  soirri  4795  relcnvtr  4918  relssdmrn  4919  cnvpom  4941  fveqeq2  5279  fvsng  5458  isose  5563  riota2f  5592  acexmidlemab  5609  0neqopab  5653  ssoprab2  5664  caovcld  5757  caovcomd  5760  caovassd  5763  caovcand  5766  caovordid  5770  caovordd  5772  caovdid  5779  caovdird  5782  caovimo  5797  grprinvlem  5798  grprinvd  5799  f1opw  5810  caofref  5835  caofinvl  5836  xpexgALT  5863  op1stg  5880  op2ndg  5881  releldm2  5914  elopabi  5924  dfmpt2  5947  smoeq  6011  tfr1onlemaccex  6069  tfrcllemaccex  6082  rdgisucinc  6106  rdg0g  6109  oacl  6177  nna0r  6195  nnmsucr  6205  ercnv  6267  swoord1  6275  swoord2  6276  eqer  6278  ider  6279  iinerm  6318  brecop  6336  en1bg  6471  fundmeng  6478  xpsneng  6492  mapen  6516  phplem3g  6526  php5  6528  php5dom  6533  findcard2d  6561  findcard2sd  6562  undifdc  6588  xpfi  6593  ordiso2  6675  mulidnq  6895  ltsonq  6904  halfnqq  6916  nqnq0pi  6944  nq02m  6971  cauappcvgprlemm  7151  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem2  7166  cauappcvgpr  7168  ltposr  7256  0idsr  7260  1idsr  7261  ax1rid  7359  ax0id  7360  axpre-ltirr  7364  mulid1  7432  1p1times  7563  cnegexlem3  7606  pncan1  7802  npcan1  7803  kcnktkm1cn  7808  apirr  8026  recexap  8064  eqneg  8141  lediv2a  8294  nn1m1nn  8378  add1p1  8601  sub1m1  8602  cnm2m1cnm3  8603  xp1d2m1eqxm1d2  8604  div4p1lem1div2  8605  nn0addcl  8644  nn0mulcl  8645  zadd2cl  8811  nn0ledivnn  9173  nltpnft  9214  ngtmnft  9215  xrrebnd  9216  xnegneg  9230  fzss1  9411  fzssp1  9415  fzshftral  9455  0elfz  9463  nn0fz0  9464  elfz0add  9465  fz0tp  9466  elfzoelz  9489  fzoval  9490  fzoss2  9514  fzossrbm1  9515  fzouzsplit  9521  elfzo1  9532  fzonn0p1  9553  fzossfzop1  9554  fzoend  9564  fzosplitsn  9575  fvinim0ffz  9583  2tnp1ge0ge0  9639  fldiv4p1lem1div2  9643  frec2uzltd  9741  frec2uzrand  9743  uzenom  9763  frecfzennn  9764  iseqeq1  9785  iseqf1olemkle  9821  iseqf1olemklt  9822  iseqf1olemqk  9831  iseqf1olemstep  9838  iseqf1olemp  9839  iseqf1oleml  9840  iseqid  9846  iseqid2  9847  iser0f  9852  m1expcl2  9879  sqoddm1div8  10006  faclbnd  10049  facubnd  10053  bcpasc  10074  hashcl  10089  omgadd  10110  reval  10182  imval  10183  crim  10191  replim  10192  rexuz3  10322  absval  10333  sqrt0  10336  resqrexlemp1rp  10338  resqrexlemfp1  10341  resqrex  10358  leabs  10406  absimle  10416  cau3  10447  dfabsmax  10549  climshft  10590  fisum  10670  negdvdsb  10718  dvdsnegb  10719  dvdsssfz1  10759  dvds1  10760  even2n  10780  oddge22np1  10787  2tp1odd  10790  ltoddhalfle  10799  m1expo  10806  m1exp1  10807  flodddiv4  10840  gcdsupex  10855  gcdsupcl  10856  ialginv  10935  ialgcvg  10936  ialgcvga  10939  ialgfx  10940  eucialgcvga  10946  lcmdvds  10967  pw2dvds  11050  oddpwdclemodd  11056  phimul  11108  evenennn  11112  bj-ex  11132  bdth  11191  bj-dcbi  11288  bj-indind  11296
  Copyright terms: Public domain W3C validator