Theorem biid 264

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 2763. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biidd  265  pm5.19  390  an21  656  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  trubitru  1599  falbifal  1602  hadcomb  1630  eqid  2763  abid1  2899  abid2f  2955  ceqsexg  3612  symdifass  4215  wecmpep  5653  sorpss  7725  epweon  7770  epweonALT  7771  tz7.49c  8429  dford2  9585  infxpen  9994  isacn  10024  dfac5  10108  dfackm  10146  pwfseq  10644  axgroth5  10804  axgroth6  10808  supmul  12182  elfz0lmr  13808  sgnneg  15133  fsum2d  15818  cbvprod  15963  cbvprodv  15964  fprod2d  16031  rpnnen2lem12  16276  isstruct  17207  oppccatid  17770  subccatid  17898  fuccatid  18024  setccatid  18136  catccatid  18158  estrccatid  18183  xpccatid  18239  lubfun  18401  lubeldm  18402  lubelss  18403  lubval  18405  lubcl  18406  lubprop  18407  lublecl  18410  lubid  18411  glbfun  18414  glbeldm  18415  glbelss  18416  glbval  18418  glbcl  18419  glbprop  18420  joinval2  18430  joineu  18431  meetval2  18444  meeteu  18445  join0  18454  meet0  18455  odulub  18456  oduglb  18458  poslubd  18462  isglbd  18560  lubun  18566  symgsssg  19532  symgfisg  19533  pmtr3ncomlem1  19538  opprsubg  20430  lmodvscl  20999  opsrtos  22208  iscnp2  23396  cbvditg  26013  ditgsplit  26020  lgsquad2  27550  2sqreuop  27626  2sqreuopnn  27627  2sqreuoplt  27628  2sqreuopltb  27629  2sqreuopnnlt  27630  2sqreuopnnltb  27631  ltssolem1  27839  addcuts  28171  mulcut  28325  elreno2  28688  nb3grpr  29732  clwwlkccat  30341  clwlkclwwlk  30353  clwwlknccat  30414  frgr3v  30626  eqid1  30818  grpoidinv  30860  stri  32609  hstri  32617  stcltrthi  32630  sq2reunnltb  32831  nmo  32836  elxrge02  33251  toslub  33293  tosglb  33295  xrsclat  33331  slmdvscl  33534  zarclsun  34260  unelldsys  34548  omssubadd  34690  ballotlemimin  34896  ballotlemfrcn0  34920  bnj1383  35219  bnj1386  35221  bnj153  35268  bnj543  35281  bnj544  35282  bnj546  35284  bnj605  35295  bnj579  35302  bnj600  35307  bnj601  35308  bnj852  35309  bnj893  35316  bnj906  35318  bnj917  35322  bnj938  35325  bnj944  35326  bnj998  35345  bnj1006  35348  bnj1029  35356  bnj1034  35358  bnj1124  35376  bnj1128  35378  bnj1127  35379  bnj1125  35380  bnj1147  35382  bnj1190  35396  bnj69  35398  bnj1204  35400  bnj1311  35412  bnj1318  35413  bnj1384  35420  bnj1408  35424  bnj1414  35425  bnj1415  35426  bnj1421  35430  bnj1423  35439  bnj1489  35444  bnj1493  35447  bnj60  35450  bnj1500  35456  bnj1522  35460  cvmliftlem11  35787  currybi  36180  dfon2  36282  brpprod3b  36377  brapply  36428  brrestrict  36441  dfrdg4  36443  cgr3permute3  36539  cgr3permute1  36540  cgr3permute2  36541  cgr3permute4  36542  cgr3permute5  36543  colinearxfr  36567  brsegle  36600  riotaeqi  36711  prodeq2si  36716  bj-prmoore  37757  bj-imdirco  37834  wl-equsal1t  38197  bicontr  38731  lub0N  39963  glb0N  39967  glbconN  40151  dalemeea  40437  dalem4  40439  dalem6  40442  dalem7  40443  dalem11  40448  dalem12  40449  dalem29  40475  dalem30  40476  dalem31N  40477  dalem32  40478  dalem33  40479  dalem34  40480  dalem35  40481  dalem36  40482  dalem37  40483  dalem40  40486  dalem46  40492  dalem47  40493  dalem49  40495  dalem50  40496  dalem52  40498  dalem53  40499  dalem54  40500  dalem56  40502  dalem58  40504  dalem59  40505  dalem62  40508  paddval  40572  4atexlemex4  40847  4atexlemex6  40848  cdleme31sdnN  41161  cdlemefr44  41199  cdleme48fv  41273  cdlemeg49lebilem  41313  cdleme50eq  41315  rngunsnply  43896  ifpbiidcor  44200  frege129d  44489  axfrege54a  44587  ismnuprim  45004  rr-grothprimbi  45005  iotaequ  45139  2uasban  45271  uunT1  45488  e2ebindVD  45620  e2ebindALT  45637  iunconnALT  45644  dfxlim2  46562  ioodvbdlimc1  46647  ioodvbdlimc2  46649  fourierdlem86  46906  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem113  46933  hoidmvlelem1  47309  hoidmvlelem3  47311  hoidmvlelem4  47312  grtriproplem  48704  grtrif1o  48707  rngccatidALTV  49037  ringccatidALTV  49071  map0cor  49633  lubeldm2d  49736  glbeldm2d  49737  lubsscl  49738  glbsscl  49739  joindm3  49747  meetdm3  49749  isclatd  49761  ipolub00  49771  ssccatid  49850  indthinc  50240  indthincALT  50241  prsthinc  50242  mndtccatid  50365  setc1onsubc  50380  2alsraln0  50595