Theorem biid 262

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 2739. (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 210	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  biidd  263  pm5.19  387  an21  650  3anbi1i  1163  3anbi2i  1164  3anbi3i  1165  trubitru  1576  falbifal  1579  hadcomb  1607  eqid  2739  abid1  2875  abid2f  2931  ceqsexg  3591  symdifass  4190  wecmpep  5610  sorpss  7671  epweon  7718  epweonALT  7719  tz7.49c  8375  dford2  9532  infxpen  9927  isacn  9957  dfac5  10042  dfackm  10080  pwfseq  10578  axgroth5  10738  axgroth6  10742  supmul  12119  elfz0lmr  13729  fsum2d  15724  cbvprod  15869  cbvprodv  15870  fprod2d  15937  rpnnen2lem12  16183  isstruct  17113  oppccatid  17676  subccatid  17804  fuccatid  17930  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  lubfun  18307  lubeldm  18308  lubelss  18309  lubval  18311  lubcl  18312  lubprop  18313  lublecl  18316  lubid  18317  glbfun  18320  glbeldm  18321  glbelss  18322  glbval  18324  glbcl  18325  glbprop  18326  joinval2  18336  joineu  18337  meetval2  18350  meeteu  18351  join0  18360  meet0  18361  odulub  18362  oduglb  18364  poslubd  18368  isglbd  18466  lubun  18472  symgsssg  19433  symgfisg  19434  pmtr3ncomlem1  19439  opprsubg  20323  lmodvscl  20868  opsrtos  22033  iscnp2  23222  cbvditg  25839  ditgsplit  25846  lgsquad2  27367  2sqreuop  27443  2sqreuopnn  27444  2sqreuoplt  27445  2sqreuopltb  27446  2sqreuopnnlt  27447  2sqreuopnnltb  27448  ltssolem1  27657  addcuts  27988  mulcut  28142  elreno2  28505  nb3grpr  29469  clwwlkccat  30078  clwlkclwwlk  30090  clwwlknccat  30151  frgr3v  30363  eqid1  30555  grpoidinv  30597  stri  32346  hstri  32354  stcltrthi  32367  sq2reunnltb  32572  nmo  32577  sgnneg  32925  elxrge02  33010  toslub  33052  tosglb  33054  xrsclat  33090  slmdvscl  33295  zarclsun  34054  unelldsys  34342  omssubadd  34484  ballotlemimin  34690  ballotlemfrcn0  34714  bnj1383  35013  bnj1386  35015  bnj153  35062  bnj543  35075  bnj544  35076  bnj546  35078  bnj605  35089  bnj579  35096  bnj600  35101  bnj601  35102  bnj852  35103  bnj893  35110  bnj906  35112  bnj917  35116  bnj938  35119  bnj944  35120  bnj998  35139  bnj1006  35142  bnj1029  35150  bnj1034  35152  bnj1124  35170  bnj1128  35172  bnj1127  35173  bnj1125  35174  bnj1147  35176  bnj1190  35190  bnj69  35192  bnj1204  35194  bnj1311  35206  bnj1318  35207  bnj1384  35214  bnj1408  35218  bnj1414  35219  bnj1415  35220  bnj1421  35224  bnj1423  35233  bnj1489  35238  bnj1493  35241  bnj60  35244  bnj1500  35250  bnj1522  35254  cvmliftlem11  35523  currybi  35916  dfon2  36018  brpprod3b  36113  brapply  36164  brrestrict  36177  dfrdg4  36179  cgr3permute3  36275  cgr3permute1  36276  cgr3permute2  36277  cgr3permute4  36278  cgr3permute5  36279  colinearxfr  36303  brsegle  36336  riotaeqi  36427  prodeq2si  36432  bj-prmoore  37473  bj-imdirco  37550  wl-equsal1t  37913  bicontr  38447  lub0N  39681  glb0N  39685  glbconN  39869  dalemeea  40155  dalem4  40157  dalem6  40160  dalem7  40161  dalem11  40166  dalem12  40167  dalem29  40193  dalem30  40194  dalem31N  40195  dalem32  40196  dalem33  40197  dalem34  40198  dalem35  40199  dalem36  40200  dalem37  40201  dalem40  40204  dalem46  40210  dalem47  40211  dalem49  40213  dalem50  40214  dalem52  40216  dalem53  40217  dalem54  40218  dalem56  40220  dalem58  40222  dalem59  40223  dalem62  40226  paddval  40290  4atexlemex4  40565  4atexlemex6  40566  cdleme31sdnN  40879  cdlemefr44  40917  cdleme48fv  40991  cdlemeg49lebilem  41031  cdleme50eq  41033  rngunsnply  43614  ifpbiidcor  43918  frege129d  44207  axfrege54a  44305  ismnuprim  44738  rr-grothprimbi  44739  iotaequ  44873  2uasban  45006  uunT1  45223  e2ebindVD  45355  e2ebindALT  45372  iunconnALT  45379  dfxlim2  46291  ioodvbdlimc1  46376  ioodvbdlimc2  46378  fourierdlem86  46635  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  hoidmvlelem1  47038  hoidmvlelem3  47040  hoidmvlelem4  47041  grtriproplem  48430  grtrif1o  48433  rngccatidALTV  48763  ringccatidALTV  48797  map0cor  49345  lubeldm2d  49448  glbeldm2d  49449  lubsscl  49450  glbsscl  49451  joindm3  49459  meetdm3  49461  isclatd  49473  ipolub00  49483  ssccatid  49562  indthinc  49952  indthincALT  49953  prsthinc  49954  mndtccatid  50077  setc1onsubc  50092