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 id1 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  pm3.2  126  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  466  simplr  467  simprl  468  simprr  469  pm3.45  514  pm5.36  527  con2i  542  notnot1  544  con3i  546  biijust  554  con3  555  con2  556  notbii  578  pm5.19  606  olc  616  orc  617  pm2.621  650  pm1.2  657  orim1i  661  orim2i  662  pm2.41  677  pm2.42  678  pm2.4  679  pm4.44  680  orim2  687  orbi1  690  pm2.38  700  pm2.74  704  pm3.2ni  710  pm4.79dc  793  biantr  841  3anim1i  1072  3anim3i  1073  mpd3an23  1214  trujust  1225  tru  1227  dftru2  1231  truimtru  1278  falimfal  1281  3impexp  1299  19.26  1343  19.8a  1455  19.9ht  1505  ax6blem  1513  19.36i  1535  19.41h  1548  equsb1  1641  sbieh  1646  dveeq2or  1670  spsbim  1697  2ax17  1731  dvelimALT  1859  dvelimfv  1860  dvelimor  1867  moanmo  1950  nfcvf  2172  necon3i  2222  nebidc  2254  vtoclgft  2572  eueq2dc  2682  cdeqcv  2726  ru  2731  sbcied2  2768  sbcralt  2802  sbcrext  2803  csbiebt  2854  csbied2  2861  cbvralcsf  2876  cbvrexcsf  2877  cbvreucsf  2878  cbvrabcsf  2879  ssid  2932  sspsstr  3018  psssstr  3019  difss2  3040  abvor0dc  3210  ssdifeq0  3273  ifbi  3314  rabsnt  3408  unisng  3560  dfnfc2  3561  a9evsep  3842  axnul  3845  intid  3923  opm  3934  opth1  3936  opth  3937  copsex4g  3947  0nelop  3948  moop2  3951  pocl  4003  swopo  4006  limeq  4052  suceq  4077  eusvnfb  4124  nn0eln0  4256  elvvuni  4319  coss1  4406  coss2  4407  dmxpm  4470  elrnmpt1  4500  soirri  4634  relcnvtr  4755  relssdmrn  4756  cnvpom  4775  fvsng  5272  isose  5373  riota2f  5401  acexmidlemab  5418  0neqopab  5461  ssoprab2  5472  caovcld  5565  caovcomd  5568  caovassd  5571  caovcand  5574  caovordid  5578  caovordd  5580  caovdid  5587  caovdird  5590  caovimo  5605  grprinvlem  5606  grprinvd  5607  f1opw  5618  caofref  5643  caofinvl  5644  xpexgALT  5671  op1stg  5688  op2ndg  5689  releldm2  5722  elopabi  5732  dfmpt2  5755  smoeq  5815  rdgisucinc  5880  oacl  5943  nna0r  5960  nnmsucr  5970  ercnv  6026  swoord1  6034  swoord2  6035  eqer  6037  ider  6038  iinerm  6077  brecop  6095  mulidnq  6234  ltsonq  6243  halfnqq  6253  nqnq0pi  6279  nq02m  6305  ltposr  6501  0idsr  6505  1idsr  6506  ax1rid  6566  ax0id  6567  axpre-ltirr  6571  mulid1  6625  1p1times  6747  cnegexlem3  6788  pncan1  6974  npcan1  6975  kcnktkm1cn  6979  apirr  7192  recexap  7219  eqneg  7293  lediv2a  7444  nn1m1nn  7515  add1p1  7752  sub1m1  7753  cnm2m1cnm3  7754  nn0addcl  7791  nn0mulcl  7792  zadd2cl  7930  bj-ex  8167  bdth  8216  bj-dcbi  8309
  Copyright terms: Public domain W3C validator