Theorem biid 261

Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also eqid 2737. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 209	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  biidd  262  pm5.19  386  an21  645  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  trubitru  1571  falbifal  1574  hadcomb  1602  eqid  2737  abid1  2873  abid2f  2930  ceqsexg  3596  symdifass  4203  wecmpep  5617  sorpss  7676  epweon  7723  epweonALT  7724  tz7.49c  8379  dford2  9535  infxpen  9930  isacn  9960  dfac5  10045  dfackm  10083  pwfseq  10581  axgroth5  10741  axgroth6  10745  supmul  12122  elfz0lmr  13732  fsum2d  15727  cbvprod  15872  cbvprodv  15873  fprod2d  15940  rpnnen2lem12  16186  isstruct  17116  oppccatid  17679  subccatid  17807  fuccatid  17933  setccatid  18045  catccatid  18067  estrccatid  18092  xpccatid  18148  lubfun  18310  lubeldm  18311  lubelss  18312  lubval  18314  lubcl  18315  lubprop  18316  lublecl  18319  lubid  18320  glbfun  18323  glbeldm  18324  glbelss  18325  glbval  18327  glbcl  18328  glbprop  18329  joinval2  18339  joineu  18340  meetval2  18353  meeteu  18354  join0  18363  meet0  18364  odulub  18365  oduglb  18367  poslubd  18371  isglbd  18469  lubun  18475  symgsssg  19436  symgfisg  19437  pmtr3ncomlem1  19442  opprsubg  20326  lmodvscl  20867  opsrtos  22048  iscnp2  23217  cbvditg  25834  ditgsplit  25841  lgsquad2  27366  2sqreuop  27442  2sqreuopnn  27443  2sqreuoplt  27444  2sqreuopltb  27445  2sqreuopnnlt  27446  2sqreuopnnltb  27447  ltssolem1  27656  addcuts  27987  mulcut  28141  elreno2  28504  nb3grpr  29468  clwwlkccat  30078  clwlkclwwlk  30090  clwwlknccat  30151  frgr3v  30363  eqid1  30555  grpoidinv  30597  stri  32346  hstri  32354  stcltrthi  32367  sq2reunnltb  32572  nmo  32577  sgnneg  32924  elxrge02  33009  toslub  33051  tosglb  33053  xrsclat  33089  slmdvscl  33293  zarclsun  34033  unelldsys  34321  omssubadd  34463  ballotlemimin  34669  ballotlemfrcn0  34693  bnj1383  34992  bnj1386  34994  bnj153  35041  bnj543  35054  bnj544  35055  bnj546  35057  bnj605  35068  bnj579  35075  bnj600  35080  bnj601  35081  bnj852  35082  bnj893  35089  bnj906  35091  bnj917  35095  bnj938  35098  bnj944  35099  bnj998  35118  bnj1006  35121  bnj1029  35129  bnj1034  35131  bnj1124  35149  bnj1128  35151  bnj1127  35152  bnj1125  35153  bnj1147  35155  bnj1190  35169  bnj69  35171  bnj1204  35173  bnj1311  35185  bnj1318  35186  bnj1384  35193  bnj1408  35197  bnj1414  35198  bnj1415  35199  bnj1421  35203  bnj1423  35212  bnj1489  35217  bnj1493  35220  bnj60  35223  bnj1500  35229  bnj1522  35233  cvmliftlem11  35496  currybi  35889  dfon2  35991  brpprod3b  36086  brapply  36137  brrestrict  36150  dfrdg4  36152  cgr3permute3  36248  cgr3permute1  36249  cgr3permute2  36250  cgr3permute4  36251  cgr3permute5  36252  colinearxfr  36276  brsegle  36309  riotaeqi  36400  prodeq2si  36405  bj-prmoore  37446  bj-imdirco  37523  wl-equsal1t  37884  bicontr  38418  lub0N  39652  glb0N  39656  glbconN  39840  dalemeea  40126  dalem4  40128  dalem6  40131  dalem7  40132  dalem11  40137  dalem12  40138  dalem29  40164  dalem30  40165  dalem31N  40166  dalem32  40167  dalem33  40168  dalem34  40169  dalem35  40170  dalem36  40171  dalem37  40172  dalem40  40175  dalem46  40181  dalem47  40182  dalem49  40184  dalem50  40185  dalem52  40187  dalem53  40188  dalem54  40189  dalem56  40191  dalem58  40193  dalem59  40194  dalem62  40197  paddval  40261  4atexlemex4  40536  4atexlemex6  40537  cdleme31sdnN  40850  cdlemefr44  40888  cdleme48fv  40962  cdlemeg49lebilem  41002  cdleme50eq  41004  rngunsnply  43618  ifpbiidcor  43922  frege129d  44211  axfrege54a  44309  ismnuprim  44742  rr-grothprimbi  44743  iotaequ  44877  2uasban  45010  uunT1  45227  e2ebindVD  45359  e2ebindALT  45376  iunconnALT  45383  dfxlim2  46297  ioodvbdlimc1  46382  ioodvbdlimc2  46384  fourierdlem86  46641  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem113  46668  hoidmvlelem1  47044  hoidmvlelem3  47046  hoidmvlelem4  47047  grtriproplem  48430  grtrif1o  48433  rngccatidALTV  48763  ringccatidALTV  48797  map0cor  49345  lubeldm2d  49448  glbeldm2d  49449  lubsscl  49450  glbsscl  49451  joindm3  49459  meetdm3  49461  isclatd  49473  ipolub00  49483  ssccatid  49562  indthinc  49952  indthincALT  49953  prsthinc  49954  mndtccatid  50077  setc1onsubc  50092