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  anidmOLD  377  anass  383  mpdan  400  mpancom  401  pm5.32  429  anbi1  442  anbi2  443  mpan10  446  simpll  469  simplr  470  simprl  471  simprr  472  pm3.45  516  pm5.36  530  con2i  545  notnot1  547  con3i  549  biijust  557  con3  558  con2  559  notbii  581  pm5.19  609  olc  619  orc  620  pm2.621  653  pm1.2  660  orim1i  664  orim2i  665  pm2.41  680  pm2.42  681  pm2.4  682  pm4.44  683  orim2  690  orbi1  693  pm2.38  703  pm2.74  707  pm3.2ni  713  pm4.79dc  797  biantr  845  3anim1i  1075  3anim3i  1076  mpd3an23  1217  trujust  1228  tru  1230  dftru2  1234  truimtru  1281  falimfal  1284  3impexp  1302  19.26  1346  19.8a  1460  19.9ht  1510  ax6blem  1518  19.36i  1540  19.41h  1553  equsb1  1646  sbieh  1651  dveeq2or  1675  spsbim  1702  2ax17  1736  dvelimALT  1864  dvelimfv  1865  dvelimor  1872  moanmo  1955  nfcvf  2177  necon3i  2227  nebidc  2259  vtoclgft  2577  eueq2dc  2687  cdeqcv  2731  ru  2736  sbcied2  2773  sbcralt  2807  sbcrext  2808  csbiebt  2859  csbied2  2866  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  ssid  2937  sspsstr  3023  psssstr  3024  difss2  3045  abvor0dc  3215  ssdifeq0  3278  ifbi  3321  rabsnt  3415  unisng  3567  dfnfc2  3568  a9evsep  3849  axnul  3852  intid  3930  opm  3941  opth1  3943  opth  3944  copsex4g  3954  0nelop  3955  moop2  3958  pocl  4010  swopo  4013  limeq  4059  suceq  4084  suctr  4104  eusvnfb  4132  nn0eln0  4264  elvvuni  4327  coss1  4414  coss2  4415  dmxpm  4478  elrnmpt1  4508  soirri  4642  relcnvtr  4763  relssdmrn  4764  cnvpom  4783  fvsng  5280  isose  5381  riota2f  5409  acexmidlemab  5426  0neqopab  5469  ssoprab2  5480  caovcld  5573  caovcomd  5576  caovassd  5579  caovcand  5582  caovordid  5586  caovordd  5588  caovdid  5595  caovdird  5598  caovimo  5613  grprinvlem  5614  grprinvd  5615  f1opw  5626  caofref  5651  caofinvl  5652  xpexgALT  5679  op1stg  5696  op2ndg  5697  releldm2  5730  elopabi  5740  dfmpt2  5763  smoeq  5823  rdgisucinc  5888  oacl  5951  nna0r  5968  nnmsucr  5978  ercnv  6034  swoord1  6042  swoord2  6043  eqer  6045  ider  6046  iinerm  6085  brecop  6103  mulidnq  6242  ltsonq  6251  halfnqq  6261  nqnq0pi  6287  nq02m  6313  ltposr  6504  0idsr  6508  1idsr  6509  ax1rid  6565  ax0id  6566  axpre-ltirr  6570  mulid1  6620  1p1times  6734  cnegexlem3  6775  pncan1  6961  npcan1  6962  kcnktkm1cn  6966  bj-ex  7148  bdth  7197  bj-d0clsepcl  7287
  Copyright terms: Public domain W3C validator