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 6 . 2 (𝜑 → (𝜑𝜑))
2 ax-1 6 . 2 (𝜑 → ((𝜑𝜑) → 𝜑))
31, 2mpd 13 1 (𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  40  pm2.43i  49  pm2.43d  50  pm2.43a  51  imim2  55  imim1i  60  imim1  76  pm2.04  82  pm2.86  100  biimprd  157  biimpcd  158  biimprcd  159  biid  170  bibi2i  226  imbi1  235  imbi2  236  bibi1  239  pm3.3  259  pm3.31  260  jctl  312  jctr  313  ancli  321  ancri  322  anc2li  327  anc2ri  328  anim12i  336  anim1i  338  anim1ci  339  anim2i  340  pm4.24  393  anass  399  mpdan  418  mpancom  419  pm5.32  449  anbi1  462  anbi2  463  mpan10  466  adantl3r  504  simpll  519  simplr  520  simprl  521  simprr  522  pm3.45  587  pm5.36  600  con2i  617  notnot  619  con3i  622  biijust  631  con3  632  con2  633  pm5.19  696  olc  701  orc  702  pm2.621  737  pm1.2  746  orim1i  750  orim2i  751  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  orim2  779  orbi1  782  pm2.38  793  pm2.74  797  pm3.2ni  803  dcbiit  825  pm4.79dc  889  biantr  937  3anim1i  1168  3anim2i  1169  3anim3i  1170  mpd3an23  1318  trujust  1334  tru  1336  dftru2  1340  truimtru  1388  falimfal  1391  3impexp  1414  19.26  1458  19.8a  1570  19.9ht  1621  ax6blem  1629  19.36i  1651  19.41h  1664  equsb1  1759  sbieh  1764  dveeq2or  1789  spsbim  1816  2ax17  1851  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  moanmo  2077  nfcvf  2304  neqne  2317  neneq  2331  necon3i  2357  nebidc  2389  r19.27v  2562  r19.28v  2563  vtoclgft  2739  rspcime  2799  eueq2dc  2860  cdeqcv  2906  ru  2911  sbcied2  2949  sbcralt  2988  sbcrext  2989  csbiebt  3042  csbied2  3050  cbvralcsf  3065  cbvrexcsf  3066  cbvreucsf  3067  cbvrabcsf  3068  ssid  3120  difss2  3207  ddifstab  3211  abvor0dc  3389  ssdifeq0  3448  rabsnt  3604  unisng  3759  dfnfc2  3760  a9evsep  4056  axnul  4059  intid  4152  opm  4162  opth1  4164  opth  4165  copsex4g  4175  0nelop  4176  moop2  4179  pocl  4231  swopo  4234  limeq  4305  suceq  4330  eusvnfb  4381  onintexmid  4493  nn0eln0  4539  elvvuni  4609  coss1  4700  coss2  4701  dmxpm  4765  elrnmpt1  4796  soirri  4939  relcnvtr  5064  relssdmrn  5065  cnvpom  5087  fveqeq2  5436  fvsng  5622  isose  5728  riota2f  5757  acexmidlemab  5774  fvoveq1  5803  0neqopab  5822  ssoprab2  5833  caovcld  5930  caovcomd  5933  caovassd  5936  caovcand  5939  caovordid  5943  caovordd  5945  caovdid  5952  caovdird  5955  caovimo  5970  grprinvlem  5971  grprinvd  5972  f1opw  5983  caofref  6009  caofinvl  6010  xpexgALT  6037  op1stg  6054  op2ndg  6055  releldm2  6089  elopabi  6099  dfmpo  6126  smoeq  6193  tfr1onlemaccex  6251  tfrcllemaccex  6264  rdgisucinc  6288  rdg0g  6291  oacl  6362  nna0r  6380  nnmsucr  6390  ercnv  6456  swoord1  6464  swoord2  6465  eqer  6467  ider  6468  iinerm  6507  brecop  6525  ixpssmapg  6628  elixpsn  6635  en1bg  6700  fundmeng  6707  xpsneng  6722  mapen  6746  phplem3g  6756  php5  6758  php5dom  6763  findcard2d  6791  findcard2sd  6792  undifdc  6818  xpfi  6824  elfir  6867  fi0  6869  ordiso2  6926  ctssdclemr  7003  ctssexmid  7030  exmidaclem  7079  djuenun  7083  cc1  7095  cc2lem  7096  mulidnq  7219  ltsonq  7228  halfnqq  7240  nqnq0pi  7268  nq02m  7295  cauappcvgprlemm  7475  cauappcvgprlemloc  7482  cauappcvgprlemladdru  7486  cauappcvgprlemladdrl  7487  cauappcvgprlem2  7490  cauappcvgpr  7492  ltposr  7593  0idsr  7597  1idsr  7598  mappsrprg  7634  ax1rid  7707  ax0id  7708  axpre-ltirr  7712  mulid1  7785  1p1times  7918  cnegexlem3  7961  pncan1  8161  npcan1  8162  kcnktkm1cn  8167  apirr  8389  recexap  8436  eqneg  8514  subrecap  8620  lediv2a  8675  nn1m1nn  8760  add1p1  8991  sub1m1  8992  cnm2m1cnm3  8993  xp1d2m1eqxm1d2  8994  div4p1lem1div2  8995  nn0addcl  9034  nn0mulcl  9035  zadd2cl  9202  nn0ledivnn  9582  nltpnft  9625  ngtmnft  9628  xrrebnd  9630  xnegneg  9644  xnegid  9670  xaddid1  9673  fzss1  9872  fzssp1  9876  fzshftral  9917  0elfz  9927  nn0fz0  9928  elfz0add  9929  fz0tp  9930  elfzoelz  9953  fzoval  9954  fzoss2  9978  fzossrbm1  9979  fzouzsplit  9985  elfzo1  9996  fzonn0p1  10017  fzossfzop1  10018  fzoend  10028  fzosplitsn  10039  fvinim0ffz  10047  2tnp1ge0ge0  10103  fldiv4p1lem1div2  10107  frec2uzltd  10205  frec2uzrand  10207  uzenom  10227  frecfzennn  10228  seqeq1  10250  iseqf1olemkle  10286  iseqf1olemklt  10287  iseqf1olemqk  10296  seq3f1olemstep  10303  seq3f1olemp  10304  seq3f1oleml  10305  seq3id  10310  seq3id2  10311  ser0f  10317  m1expcl2  10344  sqoddm1div8  10473  faclbnd  10517  facubnd  10521  bcpasc  10542  hashcl  10557  omgadd  10578  reval  10651  imval  10652  crim  10660  replim  10661  rexuz3  10792  absval  10803  sqrt0  10806  resqrexlemp1rp  10808  resqrexlemfp1  10811  resqrex  10828  abs00  10866  leabs  10876  absimle  10886  cau3  10917  dfabsmax  11019  climshft  11103  fsum3  11186  fsumcnv  11236  fsumiun  11276  binom  11283  bcxmaslem1  11287  isumshft  11289  arisum  11297  arisum2  11298  trireciplem  11299  trirecip  11300  geo2sum2  11314  geo2lim  11315  prodf1f  11342  ege2le3  11407  ef4p  11430  efgt1p2  11431  efgt1p  11432  sinval  11438  cosval  11439  negdvdsb  11538  dvdsnegb  11539  dvdsssfz1  11579  dvds1  11580  even2n  11600  oddge22np1  11607  2tp1odd  11610  ltoddhalfle  11619  m1expo  11626  m1exp1  11627  flodddiv4  11660  gcdsupex  11675  gcdsupcl  11676  alginv  11757  algcvg  11758  algcvga  11761  algfx  11762  eucalgcvga  11768  lcmdvds  11789  pw2dvds  11873  oddpwdclemodd  11879  phimul  11931  evenennn  11935  ennnfonelemp1  11948  ennnfonelemkh  11954  ennnfonelemnn0  11964  strslfv2  12034  strslfv  12035  ressid  12052  tsettps  12237  baspartn  12249  eltg  12253  en1top  12278  isopn3  12326  resttopon  12372  lmbr2  12415  cnptopresti  12439  cndis  12442  lmfpm  12444  lmcl  12446  lmff  12450  txswaphmeolem  12521  ispsmet  12524  psmet0  12528  xmetunirn  12559  bl2in  12604  metrest  12707  cncfmptid  12784  negcncf  12789  negfcncf  12790  limccl  12829  eldvap  12852  dvexp  12876  dveflem  12888  dvef  12889  logge0b  13012  logle1b  13014  logcxp  13019  bj-ex  13133  bdth  13193  bj-indind  13294
  Copyright terms: Public domain W3C validator