ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  id Structured version   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  notnot1  559  con3i  561  biijust  569  con3  570  con2  571  notbii  593  pm5.19  621  olc  631  orc  632  pm2.621  665  pm1.2  672  orim1i  676  orim2i  677  pm2.41  692  pm2.42  693  pm2.4  694  pm4.44  695  orim2  702  orbi1  705  pm2.38  715  pm2.74  719  pm3.2ni  725  pm4.79dc  808  biantr  858  3anim1i  1089  3anim2i  1090  3anim3i  1091  mpd3an23  1233  trujust  1244  tru  1246  dftru2  1250  truimtru  1297  falimfal  1300  3impexp  1323  19.26  1367  19.8a  1479  19.9ht  1529  ax6blem  1537  19.36i  1559  19.41h  1572  equsb1  1665  sbieh  1670  dveeq2or  1694  spsbim  1721  2ax17  1755  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  moanmo  1974  nfcvf  2196  necon3i  2247  nebidc  2279  vtoclgft  2598  eueq2dc  2708  cdeqcv  2752  ru  2757  sbcied2  2794  sbcralt  2828  sbcrext  2829  csbiebt  2880  csbied2  2887  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  ssid  2958  sspsstr  3044  psssstr  3045  difss2  3066  abvor0dc  3236  ssdifeq0  3299  ifbi  3342  rabsnt  3436  unisng  3588  dfnfc2  3589  a9evsep  3870  axnul  3873  intid  3951  opm  3962  opth1  3964  opth  3965  copsex4g  3975  0nelop  3976  moop2  3979  pocl  4031  swopo  4034  limeq  4080  suceq  4105  eusvnfb  4152  nn0eln0  4284  elvvuni  4347  coss1  4434  coss2  4435  dmxpm  4498  elrnmpt1  4528  soirri  4662  relcnvtr  4783  relssdmrn  4784  cnvpom  4803  fvsng  5302  isose  5403  riota2f  5432  acexmidlemab  5449  0neqopab  5492  ssoprab2  5503  caovcld  5596  caovcomd  5599  caovassd  5602  caovcand  5605  caovordid  5609  caovordd  5611  caovdid  5618  caovdird  5621  caovimo  5636  grprinvlem  5637  grprinvd  5638  f1opw  5649  caofref  5674  caofinvl  5675  xpexgALT  5702  op1stg  5719  op2ndg  5720  releldm2  5753  elopabi  5763  dfmpt2  5786  smoeq  5846  rdgisucinc  5912  rdg0g  5915  oacl  5979  nna0r  5996  nnmsucr  6006  ercnv  6063  swoord1  6071  swoord2  6072  eqer  6074  ider  6075  iinerm  6114  brecop  6132  en1bg  6216  fundmeng  6223  xpsneng  6232  mulidnq  6373  ltsonq  6382  halfnqq  6393  nqnq0pi  6421  nq02m  6448  cauappcvgprlemm  6617  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem2  6632  cauappcvgpr  6634  ltposr  6691  0idsr  6695  1idsr  6696  ax1rid  6761  ax0id  6762  axpre-ltirr  6766  mulid1  6822  1p1times  6944  cnegexlem3  6985  pncan1  7171  npcan1  7172  kcnktkm1cn  7176  apirr  7389  recexap  7416  eqneg  7490  lediv2a  7642  nn1m1nn  7713  add1p1  7951  sub1m1  7952  cnm2m1cnm3  7953  nn0addcl  7993  nn0mulcl  7994  zadd2cl  8143  nltpnft  8500  ngtmnft  8501  xrrebnd  8502  xnegneg  8516  fzss1  8696  fzssp1  8700  fzshftral  8740  0elfz  8747  nn0fz0  8748  elfz0add  8749  fz0tp  8751  elfzoelz  8774  fzoval  8775  fzoss2  8798  fzossrbm1  8799  fzouzsplit  8805  elfzo1  8816  fzonn0p1  8837  fzossfzop1  8838  fzoend  8848  fzosplitsn  8859  frec2uzltd  8870  frec2uzrand  8872  uzenom  8883  frecfzennn  8884  iseqeq1  8894  m1expcl2  8931  reval  9077  imval  9078  crim  9086  replim  9087  absval  9210  sqrt0  9213  bj-ex  9237  bdth  9286  bj-dcbi  9383  bj-indind  9391
  Copyright terms: Public domain W3C validator