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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (φ → (φ → φ))
2		ax-1 6	. 2 ⊢ (φ → ((φ → φ) → φ))
3	1, 2	mpd 14	1 ⊢ (φ → φ)

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  2512  necon3i  2556  nebi  2588  vtoclgft  2906  eueq2  3011  ru  3046  sbcied2  3084  sbcralt  3119  sbcrext  3120  csbiebt  3173  csbied2  3180  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  ssid  3291  difss2  3396  abvor0  3568  ssdifeq0  3633  rabsnt  3798  unisng  3909  dfnfc2  3910  iununi  4051  pw1eqadj  4333  eladdc  4399  nncaddccl  4420  tfincl  4493  phi11lem1  4596  copsex4g  4611  coss1  4873  coss2  4874  dmxpid  4925  rnxpid  5055  fvi  5443  fvsng  5447  1st2nd2  5517  caovmo  5646  clos1induct  5881  refd  5928  eqer  5962  erdmrn  5966  pmfun  6016  elmapi  6017  fundmeng  6045  xpsneng  6051  enprmaplem5  6081  nenpw1pwlem2  6086  ncseqnc  6129  mucass  6136  mucid1  6144  ce0nnul  6178  ce0addcnnul  6180  dflec2  6211  ce2lt  6221  nnltp1c  6263  nncdiv3  6278  nnc3n3p1  6279  spacis  6289  nchoicelem1  6290  nchoicelem2  6291  nchoicelem8  6297  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309  elcan  6330