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  843  biantr  894  3anim1i  1125  3anim2i  1126  3anim3i  1127  mpd3an23  1271  trujust  1287  tru  1289  dftru2  1293  truimtru  1341  falimfal  1344  3impexp  1367  19.26  1411  19.8a  1523  19.9ht  1573  ax6blem  1581  19.36i  1603  19.41h  1616  equsb1  1709  sbieh  1714  dveeq2or  1738  spsbim  1765  2ax17  1800  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  moanmo  2019  nfcvf  2241  neqne  2254  neneq  2268  necon3i  2294  nebidc  2326  vtoclgft  2650  eueq2dc  2766  cdeqcv  2810  ru  2815  sbcied2  2852  sbcralt  2891  sbcrext  2892  csbiebt  2943  csbied2  2950  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  ssid  3019  difss2  3101  ddifstab  3105  abvor0dc  3270  ssdifeq0  3326  ifbi  3371  rabsnt  3469  unisng  3620  dfnfc2  3621  a9evsep  3902  axnul  3905  intid  3981  opm  3991  opth1  3993  opth  3994  copsex4g  4004  0nelop  4005  moop2  4008  pocl  4060  swopo  4063  limeq  4134  suceq  4159  eusvnfb  4206  onintexmid  4317  nn0eln0  4361  elvvuni  4424  coss1  4513  coss2  4514  dmxpm  4577  elrnmpt1  4607  soirri  4743  relcnvtr  4864  relssdmrn  4865  cnvpom  4884  fvsng  5385  isose  5485  riota2f  5514  acexmidlemab  5531  0neqopab  5575  ssoprab2  5586  caovcld  5679  caovcomd  5682  caovassd  5685  caovcand  5688  caovordid  5692  caovordd  5694  caovdid  5701  caovdird  5704  caovimo  5719  grprinvlem  5720  grprinvd  5721  f1opw  5732  caofref  5757  caofinvl  5758  xpexgALT  5785  op1stg  5802  op2ndg  5803  releldm2  5836  elopabi  5846  dfmpt2  5869  smoeq  5933  tfr1onlemaccex  5991  tfrcllemaccex  6004  rdgisucinc  6028  rdg0g  6031  oacl  6098  nna0r  6115  nnmsucr  6125  ercnv  6186  swoord1  6194  swoord2  6195  eqer  6197  ider  6198  iinerm  6237  brecop  6255  en1bg  6339  fundmeng  6346  xpsneng  6356  phplem3g  6381  php5  6383  php5dom  6388  findcard2d  6415  findcard2sd  6416  undiffi  6433  ordiso2  6495  mulidnq  6630  ltsonq  6639  halfnqq  6651  nqnq0pi  6679  nq02m  6706  cauappcvgprlemm  6886  cauappcvgprlemloc  6893  cauappcvgprlemladdru  6897  cauappcvgprlemladdrl  6898  cauappcvgprlem2  6901  cauappcvgpr  6903  ltposr  6991  0idsr  6995  1idsr  6996  ax1rid  7094  ax0id  7095  axpre-ltirr  7099  mulid1  7167  1p1times  7298  cnegexlem3  7341  pncan1  7537  npcan1  7538  kcnktkm1cn  7543  apirr  7761  recexap  7799  eqneg  7876  lediv2a  8029  nn1m1nn  8113  add1p1  8336  sub1m1  8337  cnm2m1cnm3  8338  xp1d2m1eqxm1d2  8339  div4p1lem1div2  8340  nn0addcl  8379  nn0mulcl  8380  zadd2cl  8546  nn0ledivnn  8908  nltpnft  8949  ngtmnft  8950  xrrebnd  8951  xnegneg  8965  fzss1  9146  fzssp1  9150  fzshftral  9190  0elfz  9198  nn0fz0  9199  elfz0add  9200  fz0tp  9201  elfzoelz  9223  fzoval  9224  fzoss2  9247  fzossrbm1  9248  fzouzsplit  9254  elfzo1  9265  fzonn0p1  9286  fzossfzop1  9287  fzoend  9297  fzosplitsn  9308  fvinim0ffz  9316  2tnp1ge0ge0  9372  fldiv4p1lem1div2  9376  frec2uzltd  9474  frec2uzrand  9476  uzenom  9496  frecfzennn  9497  iseqeq1  9513  iseqid  9552  iseqid2  9553  iser0f  9558  m1expcl2  9584  sqoddm1div8  9711  faclbnd  9754  facubnd  9758  bcpasc  9779  sizecl  9794  omgadd  9815  reval  9863  imval  9864  crim  9872  replim  9873  rexuz3  10003  absval  10014  sqrt0  10017  resqrexlemp1rp  10019  resqrexlemfp1  10022  resqrex  10039  leabs  10087  absimle  10097  cau3  10128  dfabsmax  10230  climshft  10270  negdvdsb  10345  dvdsnegb  10346  dvdsssfz1  10386  dvds1  10387  even2n  10407  oddge22np1  10414  2tp1odd  10417  ltoddhalfle  10426  m1expo  10433  m1exp1  10434  flodddiv4  10467  gcdsupex  10482  gcdsupcl  10483  ialginv  10562  ialgcvg  10563  ialgcvga  10566  ialgfx  10567  eucialgcvga  10573  lcmdvds  10594  pw2dvds  10677  oddpwdclemodd  10683  bj-ex  10709  bdth  10765  bj-dcbi  10862  bj-indind  10870
  Copyright terms: Public domain W3C validator