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 2731. (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  644  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  trubitru  1570  falbifal  1573  hadcomb  1601  eqid  2731  abid1  2867  abid2f  2925  ceqsexg  3603  ralab  3647  symdifass  4209  wecmpep  5606  sorpss  7661  epweon  7708  epweonALT  7709  tz7.49c  8365  dford2  9510  infxpen  9905  isacn  9935  dfac5  10020  dfackm  10058  pwfseq  10555  axgroth5  10715  axgroth6  10719  supmul  12094  elfz0lmr  13683  fsum2d  15678  cbvprod  15820  cbvprodv  15821  fprod2d  15888  rpnnen2lem12  16134  isstruct  17063  oppccatid  17625  subccatid  17753  fuccatid  17879  setccatid  17991  catccatid  18013  estrccatid  18038  xpccatid  18094  lubfun  18256  lubeldm  18257  lubelss  18258  lubval  18260  lubcl  18261  lubprop  18262  lublecl  18265  lubid  18266  glbfun  18269  glbeldm  18270  glbelss  18271  glbval  18273  glbcl  18274  glbprop  18275  joinval2  18285  joineu  18286  meetval2  18299  meeteu  18300  join0  18309  meet0  18310  odulub  18311  oduglb  18313  poslubd  18317  isglbd  18415  lubun  18421  symgsssg  19379  symgfisg  19380  pmtr3ncomlem1  19385  opprsubg  20270  lmodvscl  20811  opsrtos  21992  iscnp2  23154  cbvditg  25782  ditgsplit  25789  lgsquad2  27324  2sqreuop  27400  2sqreuopnn  27401  2sqreuoplt  27402  2sqreuopltb  27403  2sqreuopnnlt  27404  2sqreuopnnltb  27405  sltsolem1  27614  addscut  27921  mulscut  28071  nb3grpr  29360  clwwlkccat  29970  clwlkclwwlk  29982  clwwlknccat  30043  frgr3v  30255  eqid1  30447  grpoidinv  30488  stri  32237  hstri  32245  stcltrthi  32258  sq2reunnltb  32464  nmo  32469  sgnneg  32816  elxrge02  32912  toslub  32954  tosglb  32956  xrsclat  32992  slmdvscl  33183  zarclsun  33883  unelldsys  34171  omssubadd  34313  ballotlemimin  34519  ballotlemfrcn0  34543  bnj1383  34843  bnj1386  34845  bnj153  34892  bnj543  34905  bnj544  34906  bnj546  34908  bnj605  34919  bnj579  34926  bnj600  34931  bnj601  34932  bnj852  34933  bnj893  34940  bnj906  34942  bnj917  34946  bnj938  34949  bnj944  34950  bnj998  34969  bnj1006  34972  bnj1029  34980  bnj1034  34982  bnj1124  35000  bnj1128  35002  bnj1127  35003  bnj1125  35004  bnj1147  35006  bnj1190  35020  bnj69  35022  bnj1204  35024  bnj1311  35036  bnj1318  35037  bnj1384  35044  bnj1408  35048  bnj1414  35049  bnj1415  35050  bnj1421  35054  bnj1423  35063  bnj1489  35068  bnj1493  35071  bnj60  35074  bnj1500  35080  bnj1522  35084  cvmliftlem11  35339  currybi  35732  dfon2  35834  brpprod3b  35929  brapply  35980  brrestrict  35991  dfrdg4  35993  cgr3permute3  36089  cgr3permute1  36090  cgr3permute2  36091  cgr3permute4  36092  cgr3permute5  36093  colinearxfr  36117  brsegle  36150  riotaeqi  36241  prodeq2si  36246  bj-prmoore  37157  bj-imdirco  37232  wl-equsal1t  37584  bicontr  38128  lub0N  39236  glb0N  39240  glbconN  39424  dalemeea  39710  dalem4  39712  dalem6  39715  dalem7  39716  dalem11  39721  dalem12  39722  dalem29  39748  dalem30  39749  dalem31N  39750  dalem32  39751  dalem33  39752  dalem34  39753  dalem35  39754  dalem36  39755  dalem37  39756  dalem40  39759  dalem46  39765  dalem47  39766  dalem49  39768  dalem50  39769  dalem52  39771  dalem53  39772  dalem54  39773  dalem56  39775  dalem58  39777  dalem59  39778  dalem62  39781  paddval  39845  4atexlemex4  40120  4atexlemex6  40121  cdleme31sdnN  40434  cdlemefr44  40472  cdleme48fv  40546  cdlemeg49lebilem  40586  cdleme50eq  40588  rngunsnply  43210  ifpbiidcor  43515  frege129d  43804  axfrege54a  43902  ismnuprim  44335  rr-grothprimbi  44336  iotaequ  44470  2uasban  44603  uunT1  44820  e2ebindVD  44952  e2ebindALT  44969  iunconnALT  44976  dfxlim2  45894  ioodvbdlimc1  45979  ioodvbdlimc2  45981  fourierdlem86  46238  fourierdlem94  46246  fourierdlem103  46255  fourierdlem104  46256  fourierdlem113  46265  hoidmvlelem1  46641  hoidmvlelem3  46643  hoidmvlelem4  46644  grtriproplem  47978  grtrif1o  47981  rngccatidALTV  48311  ringccatidALTV  48345  map0cor  48894  lubeldm2d  48997  glbeldm2d  48998  lubsscl  48999  glbsscl  49000  joindm3  49008  meetdm3  49010  isclatd  49022  ipolub00  49032  ssccatid  49112  indthinc  49502  indthincALT  49503  prsthinc  49504  mndtccatid  49627  setc1onsubc  49642