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  com12  27  pm2.27  35  pm2.43i  43  pm2.43d  44  pm2.43a  45  imim2  49  imim1i  54  imim1  70  pm2.04  76  pm2.86  94  biimprd  147  biimpcd  148  biimprcd  149  biid  160  bibi2i  216  imbi1  225  imbi2  226  bibi1  229  pm3.3  248  pm3.31  249  jctl  297  jctr  298  ancli  306  ancri  307  anc2li  312  anc2ri  313  anim12i  321  anim1i  323  anim2i  324  pm4.24  375  anass  381  mpdan  398  mpancom  399  pm5.32  426  anbi1  439  anbi2  440  mpan10  443  simpll  481  simplr  482  simprl  483  simprr  484  pm3.45  529  pm5.36  542  con2i  557  notnot  559  con3i  562  biijust  570  con3  571  con2  572  notbii  594  pm5.19  622  olc  632  orc  633  pm2.621  666  pm1.2  673  orim1i  677  orim2i  678  pm2.41  693  pm2.42  694  pm2.4  695  pm4.44  696  orim2  703  orbi1  706  pm2.38  716  pm2.74  720  pm3.2ni  726  pm4.79dc  809  biantr  859  3anim1i  1090  3anim2i  1091  3anim3i  1092  mpd3an23  1234  trujust  1245  tru  1247  dftru2  1251  truimtru  1300  falimfal  1303  3impexp  1326  19.26  1370  19.8a  1482  19.9ht  1532  ax6blem  1540  19.36i  1562  19.41h  1575  equsb1  1668  sbieh  1673  dveeq2or  1697  spsbim  1724  2ax17  1758  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  moanmo  1977  nfcvf  2199  neqne  2214  neneq  2227  necon3i  2253  nebidc  2285  vtoclgft  2604  eueq2dc  2714  cdeqcv  2758  ru  2763  sbcied2  2800  sbcralt  2834  sbcrext  2835  csbiebt  2886  csbied2  2893  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  ssid  2964  sspsstr  3050  psssstr  3051  difss2  3072  abvor0dc  3242  ssdifeq0  3305  ifbi  3348  rabsnt  3445  unisng  3597  dfnfc2  3598  a9evsep  3879  axnul  3882  intid  3960  opm  3971  opth1  3973  opth  3974  copsex4g  3984  0nelop  3985  moop2  3988  pocl  4040  swopo  4043  limeq  4114  suceq  4139  eusvnfb  4186  onintexmid  4297  nn0eln0  4341  elvvuni  4404  coss1  4491  coss2  4492  dmxpm  4555  elrnmpt1  4585  soirri  4719  relcnvtr  4840  relssdmrn  4841  cnvpom  4860  fvsng  5359  isose  5460  riota2f  5489  acexmidlemab  5506  0neqopab  5550  ssoprab2  5561  caovcld  5654  caovcomd  5657  caovassd  5660  caovcand  5663  caovordid  5667  caovordd  5669  caovdid  5676  caovdird  5679  caovimo  5694  grprinvlem  5695  grprinvd  5696  f1opw  5707  caofref  5732  caofinvl  5733  xpexgALT  5760  op1stg  5777  op2ndg  5778  releldm2  5811  elopabi  5821  dfmpt2  5844  smoeq  5905  rdgisucinc  5972  rdg0g  5975  oacl  6040  nna0r  6057  nnmsucr  6067  ercnv  6127  swoord1  6135  swoord2  6136  eqer  6138  ider  6139  iinerm  6178  brecop  6196  en1bg  6280  fundmeng  6287  xpsneng  6296  phplem3g  6319  php5  6321  php5dom  6325  findcard2d  6348  findcard2sd  6349  ordiso2  6357  mulidnq  6487  ltsonq  6496  halfnqq  6508  nqnq0pi  6536  nq02m  6563  cauappcvgprlemm  6743  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem2  6758  cauappcvgpr  6760  ltposr  6848  0idsr  6852  1idsr  6853  ax1rid  6951  ax0id  6952  axpre-ltirr  6956  mulid1  7024  1p1times  7147  cnegexlem3  7188  pncan1  7375  npcan1  7376  kcnktkm1cn  7380  apirr  7596  recexap  7634  eqneg  7708  lediv2a  7861  nn1m1nn  7932  add1p1  8174  sub1m1  8175  cnm2m1cnm3  8176  div4p1lem1div2  8177  nn0addcl  8217  nn0mulcl  8218  zadd2cl  8367  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  xnegneg  8746  fzss1  8926  fzssp1  8930  fzshftral  8970  0elfz  8977  nn0fz0  8978  elfz0add  8979  fz0tp  8981  elfzoelz  9004  fzoval  9005  fzoss2  9028  fzossrbm1  9029  fzouzsplit  9035  elfzo1  9046  fzonn0p1  9067  fzossfzop1  9068  fzoend  9078  fzosplitsn  9089  fvinim0ffz  9096  2tnp1ge0ge0  9143  fldiv4p1lem1div2  9147  frec2uzltd  9189  frec2uzrand  9191  uzenom  9202  frecfzennn  9203  iseqeq1  9214  iseqid  9247  iser0f  9251  m1expcl2  9277  reval  9449  imval  9450  crim  9458  replim  9459  rexuz3  9588  absval  9599  sqrt0  9602  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrex  9624  leabs  9672  absimle  9680  cau3  9711  climshft  9825  ialginv  9886  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  bj-ex  9902  bdth  9951  bj-dcbi  10048  bj-indind  10056
  Copyright terms: Public domain W3C validator