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 2729. (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  1569  falbifal  1572  hadcomb  1600  eqid  2729  abid1  2864  abid2f  2922  ceqsexg  3616  ralab  3661  symdifass  4221  wecmpep  5623  sorpss  7684  epweon  7731  epweonALT  7732  tz7.49c  8391  dford2  9549  infxpen  9943  isacn  9973  dfac5  10058  dfackm  10096  pwfseq  10593  axgroth5  10753  axgroth6  10757  supmul  12131  elfz0lmr  13719  fsum2d  15713  cbvprod  15855  cbvprodv  15856  fprod2d  15923  rpnnen2lem12  16169  isstruct  17098  oppccatid  17660  subccatid  17788  fuccatid  17914  setccatid  18026  catccatid  18048  estrccatid  18073  xpccatid  18129  lubfun  18291  lubeldm  18292  lubelss  18293  lubval  18295  lubcl  18296  lubprop  18297  lublecl  18300  lubid  18301  glbfun  18304  glbeldm  18305  glbelss  18306  glbval  18308  glbcl  18309  glbprop  18310  joinval2  18320  joineu  18321  meetval2  18334  meeteu  18335  join0  18344  meet0  18345  odulub  18346  oduglb  18348  poslubd  18352  isglbd  18450  lubun  18456  symgsssg  19381  symgfisg  19382  pmtr3ncomlem1  19387  opprsubg  20272  lmodvscl  20816  opsrtos  21997  iscnp2  23159  cbvditg  25788  ditgsplit  25795  lgsquad2  27330  2sqreuop  27406  2sqreuopnn  27407  2sqreuoplt  27408  2sqreuopltb  27409  2sqreuopnnlt  27410  2sqreuopnnltb  27411  sltsolem1  27620  addscut  27925  mulscut  28075  nb3grpr  29362  clwwlkccat  29969  clwlkclwwlk  29981  clwwlknccat  30042  frgr3v  30254  eqid1  30446  grpoidinv  30487  stri  32236  hstri  32244  stcltrthi  32257  sq2reunnltb  32464  nmo  32469  sgnneg  32808  elxrge02  32902  toslub  32945  tosglb  32947  xrsclat  32995  slmdvscl  33183  zarclsun  33853  unelldsys  34141  omssubadd  34284  ballotlemimin  34490  ballotlemfrcn0  34514  bnj1383  34814  bnj1386  34816  bnj153  34863  bnj543  34876  bnj544  34877  bnj546  34879  bnj605  34890  bnj579  34897  bnj600  34902  bnj601  34903  bnj852  34904  bnj893  34911  bnj906  34913  bnj917  34917  bnj938  34920  bnj944  34921  bnj998  34940  bnj1006  34943  bnj1029  34951  bnj1034  34953  bnj1124  34971  bnj1128  34973  bnj1127  34974  bnj1125  34975  bnj1147  34977  bnj1190  34991  bnj69  34993  bnj1204  34995  bnj1311  35007  bnj1318  35008  bnj1384  35015  bnj1408  35019  bnj1414  35020  bnj1415  35021  bnj1421  35025  bnj1423  35034  bnj1489  35039  bnj1493  35042  bnj60  35045  bnj1500  35051  bnj1522  35055  cvmliftlem11  35275  currybi  35668  dfon2  35773  brpprod3b  35868  brapply  35919  brrestrict  35930  dfrdg4  35932  cgr3permute3  36028  cgr3permute1  36029  cgr3permute2  36030  cgr3permute4  36031  cgr3permute5  36032  colinearxfr  36056  brsegle  36089  riotaeqi  36180  prodeq2si  36185  bj-prmoore  37096  bj-imdirco  37171  wl-equsal1t  37523  bicontr  38067  lub0N  39175  glb0N  39179  glbconN  39363  glbconNOLD  39364  dalemeea  39650  dalem4  39652  dalem6  39655  dalem7  39656  dalem11  39661  dalem12  39662  dalem29  39688  dalem30  39689  dalem31N  39690  dalem32  39691  dalem33  39692  dalem34  39693  dalem35  39694  dalem36  39695  dalem37  39696  dalem40  39699  dalem46  39705  dalem47  39706  dalem49  39708  dalem50  39709  dalem52  39711  dalem53  39712  dalem54  39713  dalem56  39715  dalem58  39717  dalem59  39718  dalem62  39721  paddval  39785  4atexlemex4  40060  4atexlemex6  40061  cdleme31sdnN  40374  cdlemefr44  40412  cdleme48fv  40486  cdlemeg49lebilem  40526  cdleme50eq  40528  rngunsnply  43151  ifpbiidcor  43456  frege129d  43745  axfrege54a  43843  ismnuprim  44276  rr-grothprimbi  44277  iotaequ  44411  2uasban  44545  uunT1  44762  e2ebindVD  44894  e2ebindALT  44911  iunconnALT  44918  dfxlim2  45839  ioodvbdlimc1  45924  ioodvbdlimc2  45926  fourierdlem86  46183  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem113  46210  hoidmvlelem1  46586  hoidmvlelem3  46588  hoidmvlelem4  46589  grtriproplem  47931  grtrif1o  47934  rngccatidALTV  48253  ringccatidALTV  48287  map0cor  48836  lubeldm2d  48939  glbeldm2d  48940  lubsscl  48941  glbsscl  48942  joindm3  48950  meetdm3  48952  isclatd  48964  ipolub00  48974  ssccatid  49054  indthinc  49444  indthincALT  49445  prsthinc  49446  mndtccatid  49569  setc1onsubc  49584