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  6355  mulidnq  6485  ltsonq  6494  halfnqq  6506  nqnq0pi  6534  nq02m  6561  cauappcvgprlemm  6741  cauappcvgprlemloc  6748  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem2  6756  cauappcvgpr  6758  ltposr  6846  0idsr  6850  1idsr  6851  ax1rid  6949  ax0id  6950  axpre-ltirr  6954  mulid1  7022  1p1times  7145  cnegexlem3  7186  pncan1  7373  npcan1  7374  kcnktkm1cn  7378  apirr  7594  recexap  7632  eqneg  7706  lediv2a  7859  nn1m1nn  7930  add1p1  8172  sub1m1  8173  cnm2m1cnm3  8174  div4p1lem1div2  8175  nn0addcl  8215  nn0mulcl  8216  zadd2cl  8365  nltpnft  8728  ngtmnft  8729  xrrebnd  8730  xnegneg  8744  fzss1  8924  fzssp1  8928  fzshftral  8968  0elfz  8975  nn0fz0  8976  elfz0add  8977  fz0tp  8979  elfzoelz  9002  fzoval  9003  fzoss2  9026  fzossrbm1  9027  fzouzsplit  9033  elfzo1  9044  fzonn0p1  9065  fzossfzop1  9066  fzoend  9076  fzosplitsn  9087  fvinim0ffz  9094  2tnp1ge0ge0  9141  fldiv4p1lem1div2  9145  frec2uzltd  9163  frec2uzrand  9165  uzenom  9176  frecfzennn  9177  iseqeq1  9188  iseqid  9221  iser0f  9225  m1expcl2  9251  reval  9423  imval  9424  crim  9432  replim  9433  rexuz3  9562  absval  9573  sqrt0  9576  resqrexlemp1rp  9578  resqrexlemfp1  9581  resqrex  9598  leabs  9646  absimle  9654  cau3  9685  climshft  9799  ialginv  9860  ialgcvg  9861  ialgcvga  9864  ialgfx  9865  bj-ex  9876  bdth  9925  bj-dcbi  10022  bj-indind  10030
  Copyright terms: Public domain W3C validator