Theorem biid 264

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 2765. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 212	1 ⊢ (𝜑 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biidd  265  pm5.19  391  an21  657  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  trubitru  1599  falbifal  1602  hadcomb  1630  eqid  2765  abid1  2901  abid2f  2957  ceqsexg  3614  symdifass  4215  wecmpep  5655  sorpss  7735  epweon  7780  epweonALT  7781  tz7.49c  8439  dford2  9596  infxpen  10014  isacn  10044  dfac5  10128  dfackm  10166  pwfseq  10664  axgroth5  10824  axgroth6  10828  supmul  12202  elfz0lmr  13829  sgnneg  15161  fsum2d  15845  cbvprod  15990  cbvprodv  15991  fprod2d  16058  rpnnen2lem12  16303  isstruct  17234  oppccatid  17797  subccatid  17925  fuccatid  18051  setccatid  18163  catccatid  18185  estrccatid  18210  xpccatid  18266  lubfun  18428  lubeldm  18429  lubelss  18430  lubval  18432  lubcl  18433  lubprop  18434  lublecl  18437  lubid  18438  glbfun  18441  glbeldm  18442  glbelss  18443  glbval  18445  glbcl  18446  glbprop  18447  joinval2  18457  joineu  18458  meetval2  18471  meeteu  18472  join0  18481  meet0  18482  odulub  18483  oduglb  18485  poslubd  18489  isglbd  18587  lubun  18593  symgsssg  19581  symgfisg  19582  pmtr3ncomlem1  19587  opprsubg  20480  lmodvscl  21049  opsrtos  22258  iscnp2  23446  cbvditg  26064  ditgsplit  26071  lgsquad2  27601  2sqreuop  27677  2sqreuopnn  27678  2sqreuoplt  27679  2sqreuopltb  27680  2sqreuopnnlt  27681  2sqreuopnnltb  27682  ltssolem1  27890  addcuts  28222  mulcut  28376  elreno2  28739  nb3grpr  29790  clwwlkccat  30408  clwlkclwwlk  30420  clwwlknccat  30481  frgr3v  30697  eqid1  30889  grpoidinv  30931  stri  32680  hstri  32688  stcltrthi  32701  sq2reunnltb  32902  nmo  32907  elxrge02  33321  toslub  33357  tosglb  33359  xrsclat  33395  slmdvscl  33598  zarclsun  34324  unelldsys  34613  omssubadd  34755  ballotlemimin  34961  ballotlemfrcn0  34985  bnj1383  35284  bnj1386  35286  bnj153  35333  bnj543  35346  bnj544  35347  bnj546  35349  bnj605  35360  bnj579  35367  bnj600  35372  bnj601  35373  bnj852  35374  bnj893  35381  bnj906  35383  bnj917  35387  bnj938  35390  bnj944  35391  bnj998  35410  bnj1006  35413  bnj1029  35421  bnj1034  35423  bnj1124  35441  bnj1128  35443  bnj1127  35444  bnj1125  35445  bnj1147  35447  bnj1190  35461  bnj69  35463  bnj1204  35465  bnj1311  35477  bnj1318  35478  bnj1384  35485  bnj1408  35489  bnj1414  35490  bnj1415  35491  bnj1421  35495  bnj1423  35504  bnj1489  35509  bnj1493  35512  bnj60  35515  bnj1500  35521  bnj1522  35525  cvmliftlem11  35824  currybi  36217  dfon2  36319  brpprod3b  36414  brapply  36465  brrestrict  36478  dfrdg4  36480  cgr3permute3  36576  cgr3permute1  36577  cgr3permute2  36578  cgr3permute4  36579  cgr3permute5  36580  colinearxfr  36604  brsegle  36637  riotaeqi  36768  prodeq2si  36773  bj-prmoore  37814  bj-imdirco  37891  wl-equsal1t  38254  bicontr  38789  lub0N  40021  glb0N  40025  glbconN  40209  dalemeea  40495  dalem4  40497  dalem6  40500  dalem7  40501  dalem11  40506  dalem12  40507  dalem29  40533  dalem30  40534  dalem31N  40535  dalem32  40536  dalem33  40537  dalem34  40538  dalem35  40539  dalem36  40540  dalem37  40541  dalem40  40544  dalem46  40550  dalem47  40551  dalem49  40553  dalem50  40554  dalem52  40556  dalem53  40557  dalem54  40558  dalem56  40560  dalem58  40562  dalem59  40563  dalem62  40566  paddval  40630  4atexlemex4  40905  4atexlemex6  40906  cdleme31sdnN  41219  cdlemefr44  41257  cdleme48fv  41331  cdlemeg49lebilem  41371  cdleme50eq  41373  rngunsnply  43954  ifpbiidcor  44258  frege129d  44547  axfrege54a  44645  ismnuprim  45062  rr-grothprimbi  45063  iotaequ  45197  2uasban  45329  uunT1  45546  e2ebindVD  45678  e2ebindALT  45695  iunconnALT  45702  dfxlim2  46620  ioodvbdlimc1  46705  ioodvbdlimc2  46707  fourierdlem86  46964  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem113  46991  hoidmvlelem1  47367  hoidmvlelem3  47369  hoidmvlelem4  47370  grtriproplem  48762  grtrif1o  48765  rngccatidALTV  49094  ringccatidALTV  49128  map0cor  49690  lubeldm2d  49793  glbeldm2d  49794  lubsscl  49795  glbsscl  49796  joindm3  49804  meetdm3  49806  isclatd  49818  ipolub00  49828  ssccatid  49907  indthinc  50297  indthincALT  50298  prsthinc  50299  mndtccatid  50422  setc1onsubc  50437  2alsraln0  50652