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 2740. (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  643  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  trubitru  1566  falbifal  1569  hadcomb  1597  eqid  2740  abid1  2881  abid2f  2942  ceqsexg  3666  ralab  3713  symdifass  4281  wecmpep  5692  sorpss  7763  epweon  7810  epweonALT  7811  tz7.49c  8502  dford2  9689  infxpen  10083  isacn  10113  dfac5  10198  dfackm  10236  pwfseq  10733  axgroth5  10893  axgroth6  10897  supmul  12267  elfz0lmr  13832  fsum2d  15819  cbvprod  15961  cbvprodv  15962  fprod2d  16029  rpnnen2lem12  16273  isstruct  17199  oppccatid  17779  subccatid  17910  fuccatid  18039  setccatid  18151  catccatid  18173  estrccatid  18200  xpccatid  18257  lubfun  18422  lubeldm  18423  lubelss  18424  lubval  18426  lubcl  18427  lubprop  18428  lublecl  18431  lubid  18432  glbfun  18435  glbeldm  18436  glbelss  18437  glbval  18439  glbcl  18440  glbprop  18441  joinval2  18451  joineu  18452  meetval2  18465  meeteu  18466  join0  18475  meet0  18476  odulub  18477  oduglb  18479  poslubd  18483  isglbd  18579  lubun  18585  symgsssg  19509  symgfisg  19510  pmtr3ncomlem1  19515  opprsubg  20378  lmodvscl  20898  opsrtos  22104  iscnp2  23268  cbvditg  25909  ditgsplit  25916  lgsquad2  27448  2sqreuop  27524  2sqreuopnn  27525  2sqreuoplt  27526  2sqreuopltb  27527  2sqreuopnnlt  27528  2sqreuopnnltb  27529  sltsolem1  27738  addscut  28029  mulscut  28176  nb3grpr  29417  clwwlkccat  30022  clwlkclwwlk  30034  clwwlknccat  30095  frgr3v  30307  eqid1  30499  grpoidinv  30540  stri  32289  hstri  32297  stcltrthi  32310  sq2reunnltb  32513  nmo  32518  elxrge02  32896  toslub  32946  tosglb  32948  xrsclat  32994  slmdvscl  33193  zarclsun  33816  unelldsys  34122  omssubadd  34265  ballotlemimin  34470  ballotlemfrcn0  34494  sgnneg  34505  bnj1383  34807  bnj1386  34809  bnj153  34856  bnj543  34869  bnj544  34870  bnj546  34872  bnj605  34883  bnj579  34890  bnj600  34895  bnj601  34896  bnj852  34897  bnj893  34904  bnj906  34906  bnj917  34910  bnj938  34913  bnj944  34914  bnj998  34933  bnj1006  34936  bnj1029  34944  bnj1034  34946  bnj1124  34964  bnj1128  34966  bnj1127  34967  bnj1125  34968  bnj1147  34970  bnj1190  34984  bnj69  34986  bnj1204  34988  bnj1311  35000  bnj1318  35001  bnj1384  35008  bnj1408  35012  bnj1414  35013  bnj1415  35014  bnj1421  35018  bnj1423  35027  bnj1489  35032  bnj1493  35035  bnj60  35038  bnj1500  35044  bnj1522  35048  cvmliftlem11  35263  currybi  35656  dfon2  35756  brpprod3b  35851  brapply  35902  brrestrict  35913  dfrdg4  35915  cgr3permute3  36011  cgr3permute1  36012  cgr3permute2  36013  cgr3permute4  36014  cgr3permute5  36015  colinearxfr  36039  brsegle  36072  riotaeqi  36163  prodeq2si  36168  bj-prmoore  37081  bj-imdirco  37156  wl-equsal1t  37496  bicontr  38040  lub0N  39145  glb0N  39149  glbconN  39333  glbconNOLD  39334  dalemeea  39620  dalem4  39622  dalem6  39625  dalem7  39626  dalem11  39631  dalem12  39632  dalem29  39658  dalem30  39659  dalem31N  39660  dalem32  39661  dalem33  39662  dalem34  39663  dalem35  39664  dalem36  39665  dalem37  39666  dalem40  39669  dalem46  39675  dalem47  39676  dalem49  39678  dalem50  39679  dalem52  39681  dalem53  39682  dalem54  39683  dalem56  39685  dalem58  39687  dalem59  39688  dalem62  39691  paddval  39755  4atexlemex4  40030  4atexlemex6  40031  cdleme31sdnN  40344  cdlemefr44  40382  cdleme48fv  40456  cdlemeg49lebilem  40496  cdleme50eq  40498  rngunsnply  43130  ifpbiidcor  43436  frege129d  43725  axfrege54a  43823  ismnuprim  44263  rr-grothprimbi  44264  iotaequ  44398  2uasban  44533  uunT1  44751  e2ebindVD  44883  e2ebindALT  44900  iunconnALT  44907  dfxlim2  45769  ioodvbdlimc1  45854  ioodvbdlimc2  45856  fourierdlem86  46113  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  hoidmvlelem1  46516  hoidmvlelem3  46518  hoidmvlelem4  46519  grtriproplem  47790  grtrif1o  47793  rngccatidALTV  47995  ringccatidALTV  48029  map0cor  48568  lubeldm2d  48638  glbeldm2d  48639  lubsscl  48640  glbsscl  48641  joindm3  48649  meetdm3  48651  isclatd  48655  ipolub00  48665  indthinc  48719  indthincALT  48720  prsthinc  48721  mndtccatid  48760