Theorem id 9

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 10.

Assertion

Ref	Expression
id	⊢ (φ → φ)

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 ⊢ (φ → (φ → φ))
2		ax-1 3	. . 3 ⊢ (φ → ((φ → φ) → φ))
3	2	a2i 8	. 2 ⊢ ((φ → (φ → φ)) → (φ → φ))
4	1, 3	ax-mp 6	1 ⊢ (φ → φ)

Syntax hints:   → wi 2

This theorem is referenced by:  idd 11  pm2.27 30  xxxid 68  bijust 126  pm4.2 148  jctl 238  jctr 239  ancli 244  ancri 245  anim1i 269  anim2i 270  orim1i 272  orim2i 273  anabs1 374  anabs7 376  imbi1 472  exmid 494  elimant 505  orbidi 510  biantr 556  bimsc1 557  con3th 573  consensus 574  hba1 698  cbv3 847  cbval 848  sbeq1 900  sbie 904  r19.15 1292  ralcom2 1314  eueq2 1429  ru 1437  unss1 1627  ssrin 1661  zfnul 1746  elpw2g 1803  copsex4g 1904  opthwiener 1914  unisng 1933  pocl 2132  sucidg 2305  ordunisuc 2339  onuninsuc 2356  unizlim 2364  orduninsuc 2365  relss 2480  dmxpid 2553  sotri 2630  relssdr 2668  fvopabgf 2874  fvopabnf 2875  fvi 2900  canth 2945  rdgzert 2982  abianfplem 2999  abianfp 3000  caoprmo 3084  1st2val 3097  oesuc 3134  oa0r 3141  om1r 3145  omordi 3164  nnmsucr 3182  xpsneng 3340  limensuc 3402  inf3lema 3460  infensuc 3484  rankonid 3538  rankr1id 3539  aceq3lem 3555  aceq5 3563  ac6lem 3575  numthlem 3598  numth 3599  zorn 3611  unxpdomlem 3649  carduni 3664  cardiun 3665  cardprc 3667  alephle 3689  cardalephex 3691  cardcf 3706  mulidpq 3863  distrlem5pr 3925  0idsr 4000  1idsr 4001  ax0id 4076  ax1id 4077  negnegt 4157  subid1t 4160  divcan1z 4226  divcan2z 4227  divcan1t 4228  divcan2t 4229  recidt 4235  divasst 4239  divcan3z 4249  divcan3t 4251  dividt 4256  div1t 4258  recrect 4260  lesub0t 4374  ltsqt 4376  eqneg 4378  2timest 4490  halfpost 4508  elnn0z 4574  om2uzlt 4654  seqlem1 4662  discrlem2 4714  nn0opth 4724  nn0opth2t 4726  sqrlem21 4751  sqrth 4757  sqsqrt 4776  absvalt 4801  cjret 4829  cjcjt 4830  absidt 4862  abslem2 4867  hiidrclt 5053  normpyth 5090  pjthlem8 5232  ococt 5253  axpjpjt 5260  chj0t 5414  chlejb1t 5429  chnlet 5431  elspansn2t 5472  cmbrt 5494  pjoml3t 5517  pjch1t 5560  pjcht 5582  pjssge0t 5636  pjdifnormt 5637  pjclem4 5653  pj3s 5659  cvexcht 5763  atexch 5769

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org