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 2763. (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  2763  abid1  2900  abid2f  2956  ceqsexg  3610  symdifass  4210  wecmpep  5650  sorpss  7776  epweon  7821  epweonALT  7822  tz7.49c  8494  dford2  9658  infxpen  10132  isacn  10162  dfac5  10246  dfackm  10284  pwfseq  10788  axgroth5  10948  axgroth6  10952  supmul  12329  elfz0lmr  13958  sgnneg  15296  fsum2d  15981  cbvprod  16126  cbvprodv  16127  fprod2d  16192  rpnnen2lem12  16437  isstruct  17374  oppccatid  17943  subccatid  18071  fuccatid  18197  setccatid  18309  catccatid  18331  estrccatid  18356  xpccatid  18412  lubfun  18574  lubeldm  18575  lubelss  18576  lubval  18578  lubcl  18579  lubprop  18580  lublecl  18583  lubid  18584  glbfun  18587  glbeldm  18588  glbelss  18589  glbval  18591  glbcl  18592  glbprop  18593  joinval2  18603  joineu  18604  meetval2  18617  meeteu  18618  join0  18627  meet0  18628  odulub  18629  oduglb  18631  poslubd  18635  isglbd  18733  lubun  18739  symgsssg  19732  symgfisg  19733  pmtr3ncomlem1  19738  opprsubg  20633  lmodvscl  21204  opsrtos  22421  iscnp2  23612  cbvditg  26229  ditgsplit  26236  rngunsnply  26693  lgsquad2  27770  2sqreuop  27846  2sqreuopnn  27847  2sqreuoplt  27848  2sqreuopltb  27849  2sqreuopnnlt  27850  2sqreuopnnltb  27851  ltssolem1  28089  addcuts  28421  mulcut  28575  elreno2  28938  nb3grpr  30020  clwwlkccat  30638  clwlkclwwlk  30650  clwwlknccat  30711  frgr3v  30933  eqid1  31125  grpoidinv  31167  stri  32916  hstri  32924  stcltrthi  32937  sq2reunnltb  33180  nmo  33185  elxrge02  33594  toslub  33630  tosglb  33632  xrsclat  33671  slmdvscl  33874  zarclsun  34613  unelldsys  34902  ballotlemimin  35249  ballotlemfrcn0  35273  bnj1383  35572  bnj1386  35574  bnj153  35621  bnj543  35634  bnj544  35635  bnj546  35637  bnj605  35648  bnj579  35655  bnj600  35660  bnj601  35661  bnj852  35662  bnj893  35669  bnj906  35671  bnj917  35675  bnj938  35678  bnj944  35679  bnj998  35698  bnj1006  35701  bnj1029  35709  bnj1034  35711  bnj1124  35729  bnj1128  35731  bnj1127  35732  bnj1125  35733  bnj1147  35735  bnj1190  35749  bnj69  35751  bnj1204  35753  bnj1311  35765  bnj1318  35766  bnj1384  35773  bnj1408  35777  bnj1414  35778  bnj1415  35779  bnj1421  35783  bnj1423  35792  bnj1489  35797  bnj1493  35800  bnj60  35803  bnj1500  35809  bnj1522  35813  cvmliftlem11  36268  currybi  36661  dfon2  36769  brpprod3b  36864  brapply  36915  brrestrict  36928  dfrdg4  36930  cgr3permute3  37027  cgr3permute1  37028  cgr3permute2  37029  cgr3permute4  37030  cgr3permute5  37031  colinearxfr  37055  brsegle  37088  riotaeqi  37203  prodeq2si  37208  bj-prmoore  38306  bj-imdirco  38379  wl-equsal1t  38742  bicontr  39280  lub0N  40512  glb0N  40516  glbconN  40700  dalemeea  40986  dalem4  40988  dalem6  40991  dalem7  40992  dalem11  40997  dalem12  40998  dalem29  41024  dalem30  41025  dalem31N  41026  dalem32  41027  dalem33  41028  dalem34  41029  dalem35  41030  dalem36  41031  dalem37  41032  dalem40  41035  dalem46  41041  dalem47  41042  dalem49  41044  dalem50  41045  dalem52  41047  dalem53  41048  dalem54  41049  dalem56  41051  dalem58  41053  dalem59  41054  dalem62  41057  paddval  41121  4atexlemex4  41396  4atexlemex6  41397  cdleme31sdnN  41710  cdlemefr44  41748  cdleme48fv  41822  cdlemeg49lebilem  41862  cdleme50eq  41864  ifpbiidcor  44736  frege129d  45024  axfrege54a  45122  ismnuprim  45539  rr-grothprimbi  45540  iotaequ  45673  2uasban  45805  uunT1  46022  e2ebindVD  46154  e2ebindALT  46171  iunconnALT  46178  dfxlim2  47131  ioodvbdlimc1  47216  ioodvbdlimc2  47218  fourierdlem86  47475  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem113  47502  hoidmvlelem1  47878  hoidmvlelem3  47880  hoidmvlelem4  47881  grtriproplem  49310  grtrif1o  49313  rngccatidALTV  49642  ringccatidALTV  49676  map0cor  50297  lubeldm2d  50403  glbeldm2d  50404  lubsscl  50405  glbsscl  50406  joindm3  50414  meetdm3  50416  isclatd  50428  ipolub00  50438  ssccatid  50517  indthinc  50928  indthincALT  50929  prsthinc  50930  mndtccatid  51056  setc1onsubc  51071  parcatid2  51094  parcatid  51095  2alsraln0  51341