NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE 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 14 1 (φφ)
Colors of variables: wff setvar 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  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  pm2.21  100  con2  108  con2i  112  notnot1  114  con1  120  con1i  121  con3  126  con3i  127  pm2.61i  156  pm2.01  160  pm2.01d  161  pm2.6  162  peirce  172  loolin  173  bijust  175  biimprd  214  biimpcd  215  biimprcd  216  biid  227  notbi  286  bibi2i  304  imbi1  313  imbi2  314  bibi1  317  pm2.621  397  exmid  404  pm2.1  406  pm3.3  431  pm3.31  432  pm3.2  434  pm3.44  497  pm1.2  499  orim1i  503  orim2i  504  jctl  525  jctr  526  ancli  534  ancri  535  anc2li  540  anc2ri  541  anim12i  549  anim1i  551  anim2i  552  pm2.41  556  pm2.42  557  pm2.4  558  pm4.44  560  pm4.79  566  pm4.24  624  anass  630  mpdan  649  mpancom  650  orbi1  686  anbi1  687  anbi2  688  simpll  730  simplr  731  simprl  732  simprr  733  pm3.45  807  orim2  814  pm2.38  815  pm3.2ni  827  pm5.36  849  oibabs  851  pm3.24  852  biantr  897  con3th  924  consensus  925  3anim1i  1138  3anim3i  1139  mpd3an23  1279  dfnot  1332  truimtru  1344  falimfal  1347  3impexp  1366  cad1  1398  had1  1402  tbw-bijust  1463  19.26  1593  2ax17  1640  exiftruOLD  1658  19.2  1659  ax12b  1689  ax7dgen  1719  19.23tOLD  1819  spimehOLD  1821  19.9tOLD  1857  19.21tOLD  1863  19.41  1879  spimed  1977  equsb1  2034  ax6  2147  moanmo  2264  nfcvf  2511  necon3i  2555  nebi  2587  vtoclgft  2905  eueq2  3010  ru  3045  sbcied2  3083  sbcralt  3118  sbcrext  3119  csbiebt  3172  csbied2  3179  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  ssid  3290  difss2  3395  abvor0  3567  ssdifeq0  3632  rabsnt  3797  unisng  3908  dfnfc2  3909  iununi  4050  pw1eqadj  4332  eladdc  4398  nncaddccl  4419  tfincl  4492  phi11lem1  4595  copsex4g  4610  coss1  4872  coss2  4873  dmxpid  4924  rnxpid  5054  fvi  5442  fvsng  5446  1st2nd2  5516  caovmo  5645  clos1induct  5880  refd  5927  eqer  5961  erdmrn  5965  pmfun  6015  elmapi  6016  fundmeng  6044  xpsneng  6050  enprmaplem5  6080  nenpw1pwlem2  6085  ncseqnc  6128  mucass  6135  mucid1  6143  ce0nnul  6177  ce0addcnnul  6179  dflec2  6210  ce2lt  6220  nnltp1c  6262  nncdiv3  6277  nnc3n3p1  6278  spacis  6288  nchoicelem1  6289  nchoicelem2  6290  nchoicelem8  6296  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  elcan  6329
  Copyright terms: Public domain W3C validator