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 2733. (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 208	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biidd  262  pm5.19  388  an21  643  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  trubitru  1571  falbifal  1574  hadcomb  1602  eqid  2733  abid1  2871  abid2f  2937  ceqsexg  3640  ralab  3686  symdifass  4250  wecmpep  5667  sorpss  7713  epweon  7757  epweonALT  7758  tz7.49c  8441  dford2  9611  infxpen  10005  isacn  10035  dfac5  10119  dfackm  10157  pwfseq  10655  axgroth5  10815  axgroth6  10819  supmul  12182  elfz0lmr  13743  fsum2d  15713  cbvprod  15855  fprod2d  15921  rpnnen2lem12  16164  isstruct  17081  oppccatid  17661  subccatid  17792  fuccatid  17918  setccatid  18030  catccatid  18052  estrccatid  18079  xpccatid  18136  lubfun  18301  lubeldm  18302  lubelss  18303  lubval  18305  lubcl  18306  lubprop  18307  lublecl  18310  lubid  18311  glbfun  18314  glbeldm  18315  glbelss  18316  glbval  18318  glbcl  18319  glbprop  18320  joinval2  18330  joineu  18331  meetval2  18344  meeteu  18345  join0  18354  meet0  18355  odulub  18356  oduglb  18358  poslubd  18362  isglbd  18458  lubun  18464  symgsssg  19328  symgfisg  19329  pmtr3ncomlem1  19334  opprsubg  20155  abvtriv  20437  lmodvscl  20477  opsrtos  21600  iscnp2  22725  cbvditg  25353  ditgsplit  25360  lgsquad2  26869  2sqreuop  26945  2sqreuopnn  26946  2sqreuoplt  26947  2sqreuopltb  26948  2sqreuopnnlt  26949  2sqreuopnnltb  26950  sltsolem1  27158  addscut  27442  mulscut  27568  nb3grpr  28619  clwwlkccat  29223  clwlkclwwlk  29235  clwwlknccat  29296  frgr3v  29508  eqid1  29700  grpoidinv  29739  stri  31488  hstri  31496  stcltrthi  31509  sq2reunnltb  31703  nmo  31708  elxrge02  32076  toslub  32121  tosglb  32123  xrsclat  32159  slmdvscl  32337  zarclsun  32788  unelldsys  33094  omssubadd  33237  ballotlemimin  33442  ballotlemfrcn0  33466  sgnneg  33477  bnj1383  33780  bnj1386  33782  bnj153  33829  bnj543  33842  bnj544  33843  bnj546  33845  bnj605  33856  bnj579  33863  bnj600  33868  bnj601  33869  bnj852  33870  bnj893  33877  bnj906  33879  bnj917  33883  bnj938  33886  bnj944  33887  bnj998  33906  bnj1006  33909  bnj1029  33917  bnj1034  33919  bnj1124  33937  bnj1128  33939  bnj1127  33940  bnj1125  33941  bnj1147  33943  bnj1190  33957  bnj69  33959  bnj1204  33961  bnj1311  33973  bnj1318  33974  bnj1384  33981  bnj1408  33985  bnj1414  33986  bnj1415  33987  bnj1421  33991  bnj1423  34000  bnj1489  34005  bnj1493  34008  bnj60  34011  bnj1500  34017  bnj1522  34021  cvmliftlem11  34224  currybi  34607  dfon2  34702  brpprod3b  34797  brapply  34848  brrestrict  34859  dfrdg4  34861  cgr3permute3  34957  cgr3permute1  34958  cgr3permute2  34959  cgr3permute4  34960  cgr3permute5  34961  colinearxfr  34985  brsegle  35018  bj-prmoore  35934  bj-imdirco  36009  wl-equsal1t  36348  bicontr  36886  lub0N  37997  glb0N  38001  glbconN  38185  glbconNOLD  38186  dalemeea  38472  dalem4  38474  dalem6  38477  dalem7  38478  dalem11  38483  dalem12  38484  dalem29  38510  dalem30  38511  dalem31N  38512  dalem32  38513  dalem33  38514  dalem34  38515  dalem35  38516  dalem36  38517  dalem37  38518  dalem40  38521  dalem46  38527  dalem47  38528  dalem49  38530  dalem50  38531  dalem52  38533  dalem53  38534  dalem54  38535  dalem56  38537  dalem58  38539  dalem59  38540  dalem62  38543  paddval  38607  4atexlemex4  38882  4atexlemex6  38883  cdleme31sdnN  39196  cdlemefr44  39234  cdleme48fv  39308  cdlemeg49lebilem  39348  cdleme50eq  39350  rngunsnply  41848  ifpbiidcor  42158  frege129d  42447  axfrege54a  42545  ismnuprim  42986  rr-grothprimbi  42987  iotaequ  43121  2uasban  43256  uunT1  43474  e2ebindVD  43606  e2ebindALT  43623  iunconnALT  43630  dfxlim2  44499  ioodvbdlimc1  44584  ioodvbdlimc2  44586  fourierdlem86  44843  fourierdlem94  44851  fourierdlem103  44860  fourierdlem104  44861  fourierdlem113  44870  hoidmvlelem1  45246  hoidmvlelem3  45248  hoidmvlelem4  45249  rngccatidALTV  46789  ringccatidALTV  46852  map0cor  47423  lubeldm2d  47493  glbeldm2d  47494  lubsscl  47495  glbsscl  47496  joindm3  47504  meetdm3  47506  isclatd  47510  ipolub00  47520  indthinc  47574  indthincALT  47575  prsthinc  47576  mndtccatid  47615