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 2736. (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  2736  abid1  2872  abid2f  2929  ceqsexg  3607  ralab  3651  symdifass  4214  wecmpep  5616  sorpss  7673  epweon  7720  epweonALT  7721  tz7.49c  8377  dford2  9529  infxpen  9924  isacn  9954  dfac5  10039  dfackm  10077  pwfseq  10575  axgroth5  10735  axgroth6  10739  supmul  12114  elfz0lmr  13699  fsum2d  15694  cbvprod  15836  cbvprodv  15837  fprod2d  15904  rpnnen2lem12  16150  isstruct  17079  oppccatid  17642  subccatid  17770  fuccatid  17896  setccatid  18008  catccatid  18030  estrccatid  18055  xpccatid  18111  lubfun  18273  lubeldm  18274  lubelss  18275  lubval  18277  lubcl  18278  lubprop  18279  lublecl  18282  lubid  18283  glbfun  18286  glbeldm  18287  glbelss  18288  glbval  18290  glbcl  18291  glbprop  18292  joinval2  18302  joineu  18303  meetval2  18316  meeteu  18317  join0  18326  meet0  18327  odulub  18328  oduglb  18330  poslubd  18334  isglbd  18432  lubun  18438  symgsssg  19396  symgfisg  19397  pmtr3ncomlem1  19402  opprsubg  20288  lmodvscl  20829  opsrtos  22012  iscnp2  23183  cbvditg  25811  ditgsplit  25818  lgsquad2  27353  2sqreuop  27429  2sqreuopnn  27430  2sqreuoplt  27431  2sqreuopltb  27432  2sqreuopnnlt  27433  2sqreuopnnltb  27434  ltssolem1  27643  addcuts  27974  mulcut  28128  elreno2  28491  nb3grpr  29455  clwwlkccat  30065  clwlkclwwlk  30077  clwwlknccat  30138  frgr3v  30350  eqid1  30542  grpoidinv  30583  stri  32332  hstri  32340  stcltrthi  32353  sq2reunnltb  32559  nmo  32564  sgnneg  32914  elxrge02  33013  toslub  33055  tosglb  33057  xrsclat  33093  slmdvscl  33296  zarclsun  34027  unelldsys  34315  omssubadd  34457  ballotlemimin  34663  ballotlemfrcn0  34687  bnj1383  34987  bnj1386  34989  bnj153  35036  bnj543  35049  bnj544  35050  bnj546  35052  bnj605  35063  bnj579  35070  bnj600  35075  bnj601  35076  bnj852  35077  bnj893  35084  bnj906  35086  bnj917  35090  bnj938  35093  bnj944  35094  bnj998  35113  bnj1006  35116  bnj1029  35124  bnj1034  35126  bnj1124  35144  bnj1128  35146  bnj1127  35147  bnj1125  35148  bnj1147  35150  bnj1190  35164  bnj69  35166  bnj1204  35168  bnj1311  35180  bnj1318  35181  bnj1384  35188  bnj1408  35192  bnj1414  35193  bnj1415  35194  bnj1421  35198  bnj1423  35207  bnj1489  35212  bnj1493  35215  bnj60  35218  bnj1500  35224  bnj1522  35228  cvmliftlem11  35489  currybi  35882  dfon2  35984  brpprod3b  36079  brapply  36130  brrestrict  36143  dfrdg4  36145  cgr3permute3  36241  cgr3permute1  36242  cgr3permute2  36243  cgr3permute4  36244  cgr3permute5  36245  colinearxfr  36269  brsegle  36302  riotaeqi  36393  prodeq2si  36398  bj-prmoore  37320  bj-imdirco  37395  wl-equsal1t  37747  bicontr  38281  lub0N  39449  glb0N  39453  glbconN  39637  dalemeea  39923  dalem4  39925  dalem6  39928  dalem7  39929  dalem11  39934  dalem12  39935  dalem29  39961  dalem30  39962  dalem31N  39963  dalem32  39964  dalem33  39965  dalem34  39966  dalem35  39967  dalem36  39968  dalem37  39969  dalem40  39972  dalem46  39978  dalem47  39979  dalem49  39981  dalem50  39982  dalem52  39984  dalem53  39985  dalem54  39986  dalem56  39988  dalem58  39990  dalem59  39991  dalem62  39994  paddval  40058  4atexlemex4  40333  4atexlemex6  40334  cdleme31sdnN  40647  cdlemefr44  40685  cdleme48fv  40759  cdlemeg49lebilem  40799  cdleme50eq  40801  rngunsnply  43411  ifpbiidcor  43715  frege129d  44004  axfrege54a  44102  ismnuprim  44535  rr-grothprimbi  44536  iotaequ  44670  2uasban  44803  uunT1  45020  e2ebindVD  45152  e2ebindALT  45169  iunconnALT  45176  dfxlim2  46092  ioodvbdlimc1  46177  ioodvbdlimc2  46179  fourierdlem86  46436  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  hoidmvlelem1  46839  hoidmvlelem3  46841  hoidmvlelem4  46842  grtriproplem  48185  grtrif1o  48188  rngccatidALTV  48518  ringccatidALTV  48552  map0cor  49100  lubeldm2d  49203  glbeldm2d  49204  lubsscl  49205  glbsscl  49206  joindm3  49214  meetdm3  49216  isclatd  49228  ipolub00  49238  ssccatid  49317  indthinc  49707  indthincALT  49708  prsthinc  49709  mndtccatid  49832  setc1onsubc  49847