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 2737. (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  1158  3anbi2i  1159  3anbi3i  1160  trubitru  1569  falbifal  1572  hadcomb  1600  eqid  2737  abid1  2878  abid2f  2936  ceqsexg  3653  ralab  3697  symdifass  4262  wecmpep  5677  sorpss  7748  epweon  7795  epweonALT  7796  tz7.49c  8486  dford2  9660  infxpen  10054  isacn  10084  dfac5  10169  dfackm  10207  pwfseq  10704  axgroth5  10864  axgroth6  10868  supmul  12240  elfz0lmr  13821  fsum2d  15807  cbvprod  15949  cbvprodv  15950  fprod2d  16017  rpnnen2lem12  16261  isstruct  17189  oppccatid  17762  subccatid  17891  fuccatid  18017  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  lubfun  18397  lubeldm  18398  lubelss  18399  lubval  18401  lubcl  18402  lubprop  18403  lublecl  18406  lubid  18407  glbfun  18410  glbeldm  18411  glbelss  18412  glbval  18414  glbcl  18415  glbprop  18416  joinval2  18426  joineu  18427  meetval2  18440  meeteu  18441  join0  18450  meet0  18451  odulub  18452  oduglb  18454  poslubd  18458  isglbd  18554  lubun  18560  symgsssg  19485  symgfisg  19486  pmtr3ncomlem1  19491  opprsubg  20352  lmodvscl  20876  opsrtos  22081  iscnp2  23247  cbvditg  25889  ditgsplit  25896  lgsquad2  27430  2sqreuop  27506  2sqreuopnn  27507  2sqreuoplt  27508  2sqreuopltb  27509  2sqreuopnnlt  27510  2sqreuopnnltb  27511  sltsolem1  27720  addscut  28011  mulscut  28158  nb3grpr  29399  clwwlkccat  30009  clwlkclwwlk  30021  clwwlknccat  30082  frgr3v  30294  eqid1  30486  grpoidinv  30527  stri  32276  hstri  32284  stcltrthi  32297  sq2reunnltb  32504  nmo  32509  elxrge02  32914  toslub  32963  tosglb  32965  xrsclat  33013  slmdvscl  33220  zarclsun  33869  unelldsys  34159  omssubadd  34302  ballotlemimin  34508  ballotlemfrcn0  34532  sgnneg  34543  bnj1383  34845  bnj1386  34847  bnj153  34894  bnj543  34907  bnj544  34908  bnj546  34910  bnj605  34921  bnj579  34928  bnj600  34933  bnj601  34934  bnj852  34935  bnj893  34942  bnj906  34944  bnj917  34948  bnj938  34951  bnj944  34952  bnj998  34971  bnj1006  34974  bnj1029  34982  bnj1034  34984  bnj1124  35002  bnj1128  35004  bnj1127  35005  bnj1125  35006  bnj1147  35008  bnj1190  35022  bnj69  35024  bnj1204  35026  bnj1311  35038  bnj1318  35039  bnj1384  35046  bnj1408  35050  bnj1414  35051  bnj1415  35052  bnj1421  35056  bnj1423  35065  bnj1489  35070  bnj1493  35073  bnj60  35076  bnj1500  35082  bnj1522  35086  cvmliftlem11  35300  currybi  35693  dfon2  35793  brpprod3b  35888  brapply  35939  brrestrict  35950  dfrdg4  35952  cgr3permute3  36048  cgr3permute1  36049  cgr3permute2  36050  cgr3permute4  36051  cgr3permute5  36052  colinearxfr  36076  brsegle  36109  riotaeqi  36200  prodeq2si  36205  bj-prmoore  37116  bj-imdirco  37191  wl-equsal1t  37543  bicontr  38087  lub0N  39190  glb0N  39194  glbconN  39378  glbconNOLD  39379  dalemeea  39665  dalem4  39667  dalem6  39670  dalem7  39671  dalem11  39676  dalem12  39677  dalem29  39703  dalem30  39704  dalem31N  39705  dalem32  39706  dalem33  39707  dalem34  39708  dalem35  39709  dalem36  39710  dalem37  39711  dalem40  39714  dalem46  39720  dalem47  39721  dalem49  39723  dalem50  39724  dalem52  39726  dalem53  39727  dalem54  39728  dalem56  39730  dalem58  39732  dalem59  39733  dalem62  39736  paddval  39800  4atexlemex4  40075  4atexlemex6  40076  cdleme31sdnN  40389  cdlemefr44  40427  cdleme48fv  40501  cdlemeg49lebilem  40541  cdleme50eq  40543  rngunsnply  43181  ifpbiidcor  43487  frege129d  43776  axfrege54a  43874  ismnuprim  44313  rr-grothprimbi  44314  iotaequ  44448  2uasban  44582  uunT1  44800  e2ebindVD  44932  e2ebindALT  44949  iunconnALT  44956  dfxlim2  45863  ioodvbdlimc1  45948  ioodvbdlimc2  45950  fourierdlem86  46207  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  hoidmvlelem1  46610  hoidmvlelem3  46612  hoidmvlelem4  46613  grtriproplem  47906  grtrif1o  47909  rngccatidALTV  48188  ringccatidALTV  48222  map0cor  48764  lubeldm2d  48855  glbeldm2d  48856  lubsscl  48857  glbsscl  48858  joindm3  48866  meetdm3  48868  isclatd  48872  ipolub00  48882  indthinc  49109  indthincALT  49110  prsthinc  49111  mndtccatid  49184