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 6 . 2 (𝜑 → (𝜑𝜑))
2 ax-1 6 . 2 (𝜑 → ((𝜑𝜑) → 𝜑))
31, 2mpd 13 1 (𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  40  pm2.43i  49  pm2.43d  50  pm2.43a  51  imim2  55  imim1i  60  imim1  76  pm2.04  82  pm2.86  101  biimprd  158  biimpcd  159  biimprcd  160  biid  171  bibi2i  227  imbi1  236  imbi2  237  bibi1  240  pm3.3  261  pm3.31  262  jctl  314  jctr  315  ancli  323  ancri  324  anc2li  329  anc2ri  330  anim12i  338  anim1i  340  anim1ci  341  anim2i  342  pm4.24  395  anass  401  mpdan  421  mpancom  422  pm5.32  453  anbi1  466  anbi2  467  mpan10  474  adantl3r  512  simpll  527  simplr  528  simprl  529  simprr  531  pm3.45  597  pm5.36  610  con2i  627  notnot  629  con3i  632  biijust  641  con3  642  con2  643  pm5.19  706  olc  711  orc  712  pm2.621  747  pm1.2  756  orim1i  760  orim2i  761  pm2.41  776  pm2.42  777  pm2.4  778  pm4.44  779  orim2  789  orbi1  792  pm2.38  803  pm2.74  807  pm3.2ni  813  biort  829  dcbiit  839  pm4.79dc  903  biantr  952  3anim1i  1185  3anim2i  1186  3anim3i  1187  mpd3an23  1339  trujust  1355  tru  1357  dftru2  1361  truimtru  1409  falimfal  1412  3impexp  1437  19.26  1481  19.8a  1590  19.9ht  1641  ax6blem  1650  19.36i  1672  19.41h  1685  equsb1  1785  sbieh  1790  dveeq2or  1816  spsbim  1843  2ax17  1878  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  moanmo  2103  nfcvf  2342  neqne  2355  neneq  2369  necon3i  2395  nebidc  2427  r19.27v  2604  r19.28v  2605  vtoclgft  2787  rspcime  2848  eueq2dc  2910  cdeqcv  2956  ru  2961  sbcied2  3000  sbcralt  3039  sbcrext  3040  csbiebt  3096  csbied2  3104  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  ssid  3175  difss2  3263  ddifstab  3267  abvor0dc  3446  ssdifeq0  3505  rabsnt  3666  unisng  3824  dfnfc2  3825  a9evsep  4122  axnul  4125  intid  4221  opm  4231  opth1  4233  opth  4234  copsex4g  4244  0nelop  4245  moop2  4248  pocl  4300  swopo  4303  limeq  4374  suceq  4399  eusvnfb  4451  onintexmid  4569  nn0eln0  4616  elvvuni  4687  coss1  4778  coss2  4779  dmxpm  4843  elrnmpt1  4874  soirri  5019  relcnvtr  5144  relssdmrn  5145  cnvpom  5167  fveqeq2  5520  fvsng  5708  isose  5816  canth  5823  riota2f  5846  acexmidlemab  5863  fvoveq1  5892  0neqopab  5914  ssoprab2  5925  caovcld  6022  caovcomd  6025  caovassd  6028  caovcand  6031  caovordid  6035  caovordd  6037  caovdid  6044  caovdird  6047  caovimo  6062  f1opw  6072  caofref  6098  caofinvl  6099  xpexgALT  6128  op1stg  6145  op2ndg  6146  releldm2  6180  elopabi  6190  dfmpo  6218  smoeq  6285  tfr1onlemaccex  6343  tfrcllemaccex  6356  rdgisucinc  6380  rdg0g  6383  oacl  6455  nna0r  6473  nnmsucr  6483  ercnv  6550  swoord1  6558  swoord2  6559  eqer  6561  ider  6562  iinerm  6601  brecop  6619  ixpssmapg  6722  elixpsn  6729  en1bg  6794  fundmeng  6801  xpsneng  6816  mapen  6840  phplem3g  6850  php5  6852  php5dom  6857  findcard2d  6885  findcard2sd  6886  undifdc  6917  xpfi  6923  elfir  6966  fi0  6968  ordiso2  7028  ctssdclemr  7105  nnnninfeq2  7121  nninfisol  7125  ctssexmid  7142  exmidaclem  7201  djuenun  7205  cc1  7252  cc2lem  7253  mulidnq  7376  ltsonq  7385  halfnqq  7397  nqnq0pi  7425  nq02m  7452  cauappcvgprlemm  7632  cauappcvgprlemloc  7639  cauappcvgprlemladdru  7643  cauappcvgprlemladdrl  7644  cauappcvgprlem2  7647  cauappcvgpr  7649  ltposr  7750  0idsr  7754  1idsr  7755  mappsrprg  7791  ax1rid  7864  ax0id  7865  axpre-ltirr  7869  mulid1  7942  1p1times  8078  cnegexlem3  8121  pncan1  8321  npcan1  8322  kcnktkm1cn  8327  apirr  8549  recexap  8596  eqneg  8675  subrecap  8782  lediv2a  8838  nn1m1nn  8923  add1p1  9154  sub1m1  9155  cnm2m1cnm3  9156  xp1d2m1eqxm1d2  9157  div4p1lem1div2  9158  nn0addcl  9197  nn0mulcl  9198  zadd2cl  9368  nn0ledivnn  9751  nltpnft  9798  ngtmnft  9801  xrrebnd  9803  xnegneg  9817  xnegid  9843  xaddid1  9846  fzss1  10046  fzssp1  10050  fzshftral  10091  0elfz  10101  nn0fz0  10102  elfz0add  10103  fz0tp  10105  elfzoelz  10130  fzoval  10131  fzoss2  10155  fzossrbm1  10156  fzouzsplit  10162  elfzo1  10173  fzonn0p1  10194  fzossfzop1  10195  fzoend  10205  fzosplitsn  10216  fvinim0ffz  10224  2tnp1ge0ge0  10284  fldiv4p1lem1div2  10288  frec2uzltd  10386  frec2uzrand  10388  uzenom  10408  frecfzennn  10409  seqeq1  10431  iseqf1olemkle  10467  iseqf1olemklt  10468  iseqf1olemqk  10477  seq3f1olemstep  10484  seq3f1olemp  10485  seq3f1oleml  10486  seq3id  10491  seq3id2  10492  ser0f  10498  m1expcl2  10525  sqoddm1div8  10656  faclbnd  10702  facubnd  10706  bcpasc  10727  hashcl  10742  omgadd  10763  reval  10839  imval  10840  crim  10848  replim  10849  rexuz3  10980  absval  10991  sqrt0  10994  resqrexlemp1rp  10996  resqrexlemfp1  10999  resqrex  11016  abs00  11054  leabs  11064  absimle  11074  cau3  11105  dfabsmax  11207  climshft  11293  fsum3  11376  fsumcnv  11426  fsumiun  11466  binom  11473  bcxmaslem1  11477  isumshft  11479  arisum  11487  arisum2  11488  trireciplem  11489  trirecip  11490  geo2sum2  11504  geo2lim  11505  prodf1f  11532  prod0  11574  fprodfac  11604  ege2le3  11660  ef4p  11683  efgt1p2  11684  efgt1p  11685  sinval  11691  cosval  11692  negdvdsb  11795  dvdsnegb  11796  dvdsssfz1  11838  dvds1  11839  even2n  11859  oddge22np1  11866  2tp1odd  11869  ltoddhalfle  11878  m1expo  11885  m1exp1  11886  flodddiv4  11919  gcdsupex  11938  gcdsupcl  11939  alginv  12027  algcvg  12028  algcvga  12031  algfx  12032  eucalgcvga  12038  lcmdvds  12059  pw2dvds  12146  oddpwdclemodd  12152  phimul  12206  eulerth  12213  pc2dvds  12309  pcz  12311  pcmpt  12321  pcmptdvds  12323  fldivp1  12326  oddprmdvds  12332  pockthg  12335  pockthi  12336  1arith  12345  zgz  12351  evenennn  12374  ennnfonelemp1  12387  ennnfonelemkh  12393  ennnfonelemnn0  12403  ssnnctlemct  12427  strslfv2  12485  strslfv  12486  ressvalsets  12503  intopsn  12675  mgmidmo  12680  ismgmid  12685  mgmlrid  12687  lidrideqd  12689  lidrididd  12690  grprinvlem  12693  grprinvd  12694  issgrp  12698  mnd1  12734  mnd1id  12735  idmhm  12747  issubm  12750  0mhm  12760  dfgrp2  12789  isgrpid2  12800  grpidd2  12801  grpinvval  12803  grpsubid1  12841  dfgrp3mlem  12854  grplactfval  12857  mhmlem  12864  mulgfvalg  12871  mulgnnp1  12877  mulgsubcl  12883  mulgnncl  12884  mulgnn0cl  12885  mulgcl  12886  mulgnn0z  12895  mulgneg2  12902  mulgmodid  12907  mgpvalg  12957  opprvalg  13063  dvdsrex  13089  dvdsrtr  13092  unitinvcl  13114  unitinvinv  13115  unitlinv  13117  unitrinv  13118  tsettps  13200  baspartn  13212  eltg  13216  en1top  13241  isopn3  13289  resttopon  13335  lmbr2  13378  cnptopresti  13402  cndis  13405  lmfpm  13407  lmcl  13409  lmff  13413  txswaphmeolem  13484  ispsmet  13487  psmet0  13491  xmetunirn  13522  bl2in  13567  metrest  13670  cncfmptid  13747  negcncf  13752  negfcncf  13753  limccl  13792  eldvap  13815  dvexp  13839  dveflem  13851  dvef  13852  logge0b  13975  logle1b  13977  logcxp  13982  zabsle1  14064  lgsval  14069  lgsfvalg  14070  lgsval2lem  14075  lgsdir2lem2  14094  lgsdir2lem4  14096  lgsdirnn0  14112  bj-ex  14167  bdth  14236  bj-indind  14337
  Copyright terms: Public domain W3C validator