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  3608  ralab  3653  symdifass  4213  wecmpep  5611  sorpss  7664  epweon  7711  epweonALT  7712  tz7.49c  8368  dford2  9516  infxpen  9908  isacn  9938  dfac5  10023  dfackm  10061  pwfseq  10558  axgroth5  10718  axgroth6  10722  supmul  12097  elfz0lmr  13685  fsum2d  15678  cbvprod  15820  cbvprodv  15821  fprod2d  15888  rpnnen2lem12  16134  isstruct  17063  oppccatid  17625  subccatid  17753  fuccatid  17879  setccatid  17991  catccatid  18013  estrccatid  18038  xpccatid  18094  lubfun  18256  lubeldm  18257  lubelss  18258  lubval  18260  lubcl  18261  lubprop  18262  lublecl  18265  lubid  18266  glbfun  18269  glbeldm  18270  glbelss  18271  glbval  18273  glbcl  18274  glbprop  18275  joinval2  18285  joineu  18286  meetval2  18299  meeteu  18300  join0  18309  meet0  18310  odulub  18311  oduglb  18313  poslubd  18317  isglbd  18415  lubun  18421  symgsssg  19346  symgfisg  19347  pmtr3ncomlem1  19352  opprsubg  20237  lmodvscl  20781  opsrtos  21962  iscnp2  23124  cbvditg  25753  ditgsplit  25760  lgsquad2  27295  2sqreuop  27371  2sqreuopnn  27372  2sqreuoplt  27373  2sqreuopltb  27374  2sqreuopnnlt  27375  2sqreuopnnltb  27376  sltsolem1  27585  addscut  27890  mulscut  28040  nb3grpr  29327  clwwlkccat  29934  clwlkclwwlk  29946  clwwlknccat  30007  frgr3v  30219  eqid1  30411  grpoidinv  30452  stri  32201  hstri  32209  stcltrthi  32222  sq2reunnltb  32429  nmo  32434  sgnneg  32778  elxrge02  32872  toslub  32915  tosglb  32917  xrsclat  32965  slmdvscl  33156  zarclsun  33837  unelldsys  34125  omssubadd  34268  ballotlemimin  34474  ballotlemfrcn0  34498  bnj1383  34798  bnj1386  34800  bnj153  34847  bnj543  34860  bnj544  34861  bnj546  34863  bnj605  34874  bnj579  34881  bnj600  34886  bnj601  34887  bnj852  34888  bnj893  34895  bnj906  34897  bnj917  34901  bnj938  34904  bnj944  34905  bnj998  34924  bnj1006  34927  bnj1029  34935  bnj1034  34937  bnj1124  34955  bnj1128  34957  bnj1127  34958  bnj1125  34959  bnj1147  34961  bnj1190  34975  bnj69  34977  bnj1204  34979  bnj1311  34991  bnj1318  34992  bnj1384  34999  bnj1408  35003  bnj1414  35004  bnj1415  35005  bnj1421  35009  bnj1423  35018  bnj1489  35023  bnj1493  35026  bnj60  35029  bnj1500  35035  bnj1522  35039  cvmliftlem11  35268  currybi  35661  dfon2  35766  brpprod3b  35861  brapply  35912  brrestrict  35923  dfrdg4  35925  cgr3permute3  36021  cgr3permute1  36022  cgr3permute2  36023  cgr3permute4  36024  cgr3permute5  36025  colinearxfr  36049  brsegle  36082  riotaeqi  36173  prodeq2si  36178  bj-prmoore  37089  bj-imdirco  37164  wl-equsal1t  37516  bicontr  38060  lub0N  39168  glb0N  39172  glbconN  39356  dalemeea  39642  dalem4  39644  dalem6  39647  dalem7  39648  dalem11  39653  dalem12  39654  dalem29  39680  dalem30  39681  dalem31N  39682  dalem32  39683  dalem33  39684  dalem34  39685  dalem35  39686  dalem36  39687  dalem37  39688  dalem40  39691  dalem46  39697  dalem47  39698  dalem49  39700  dalem50  39701  dalem52  39703  dalem53  39704  dalem54  39705  dalem56  39707  dalem58  39709  dalem59  39710  dalem62  39713  paddval  39777  4atexlemex4  40052  4atexlemex6  40053  cdleme31sdnN  40366  cdlemefr44  40404  cdleme48fv  40478  cdlemeg49lebilem  40518  cdleme50eq  40520  rngunsnply  43142  ifpbiidcor  43447  frege129d  43736  axfrege54a  43834  ismnuprim  44267  rr-grothprimbi  44268  iotaequ  44402  2uasban  44536  uunT1  44753  e2ebindVD  44885  e2ebindALT  44902  iunconnALT  44909  dfxlim2  45829  ioodvbdlimc1  45914  ioodvbdlimc2  45916  fourierdlem86  46173  fourierdlem94  46181  fourierdlem103  46190  fourierdlem104  46191  fourierdlem113  46200  hoidmvlelem1  46576  hoidmvlelem3  46578  hoidmvlelem4  46579  grtriproplem  47923  grtrif1o  47926  rngccatidALTV  48256  ringccatidALTV  48290  map0cor  48839  lubeldm2d  48942  glbeldm2d  48943  lubsscl  48944  glbsscl  48945  joindm3  48953  meetdm3  48955  isclatd  48967  ipolub00  48977  ssccatid  49057  indthinc  49447  indthincALT  49448  prsthinc  49449  mndtccatid  49572  setc1onsubc  49587