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 2798. (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 212	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biidd  265  pm5.19  391  an21  643  3anbi1i  1154  3anbi2i  1155  3anbi3i  1156  trubitru  1567  falbifal  1570  hadcomaOLD  1601  hadcomb  1602  sb6fALT  2578  sbi2ALT  2583  sbrimALT  2585  sbanALT  2586  sbbiALT  2587  sbieALT  2589  sbiedALT  2590  sbco2ALT  2591  sb7fALT  2592  eqid  2798  abid1  2931  ceqsexg  3594  symdifass  4178  wecmpep  5511  sorpss  7434  epweon  7477  tz7.49c  8065  dford2  9067  infxpen  9425  isacn  9455  dfac5  9539  dfackm  9577  pwfseq  10075  axgroth5  10235  axgroth6  10239  supmul  11600  elfz0lmr  13147  fsum2d  15118  cbvprod  15261  fprod2d  15327  rpnnen2lem12  15570  isstruct  16488  oppccatid  16981  subccatid  17108  fuccatid  17231  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  lubfun  17582  lubeldm  17583  lubelss  17584  lubval  17586  lubcl  17587  lubprop  17588  lublecl  17591  lubid  17592  glbfun  17595  glbeldm  17596  glbelss  17597  glbval  17599  glbcl  17600  glbprop  17601  joinval2  17611  joineu  17612  meetval2  17625  meeteu  17626  isglbd  17719  lubun  17725  meet0  17739  join0  17740  oduglb  17741  odulub  17743  poslubd  17750  symgsssg  18587  symgfisg  18588  pmtr3ncomlem1  18593  opprsubg  19382  abvtriv  19605  lmodvscl  19644  opsrtos  20725  iscnp2  21844  cbvditg  24457  ditgsplit  24464  lgsquad2  25970  2sqreuop  26046  2sqreuopnn  26047  2sqreuoplt  26048  2sqreuopltb  26049  2sqreuopnnlt  26050  2sqreuopnnltb  26051  nb3grpr  27172  clwwlkccat  27775  clwlkclwwlk  27787  clwwlknccat  27848  frgr3v  28060  eqid1  28252  grpoidinv  28291  stri  30040  hstri  30048  stcltrthi  30061  sq2reunnltb  30255  nmo  30261  elxrge02  30634  toslub  30681  tosglb  30683  xrsclat  30714  slmdvscl  30892  zarclsun  31223  unelldsys  31527  omssubadd  31668  ballotlemimin  31873  ballotlemfrcn0  31897  sgnneg  31908  bnj1383  32213  bnj1386  32215  bnj153  32262  bnj543  32275  bnj544  32276  bnj546  32278  bnj605  32289  bnj579  32296  bnj600  32301  bnj601  32302  bnj852  32303  bnj893  32310  bnj906  32312  bnj917  32316  bnj938  32319  bnj944  32320  bnj998  32339  bnj1006  32342  bnj1029  32350  bnj1034  32352  bnj1124  32370  bnj1128  32372  bnj1127  32373  bnj1125  32374  bnj1147  32376  bnj1190  32390  bnj69  32392  bnj1204  32394  bnj1311  32406  bnj1318  32407  bnj1384  32414  bnj1408  32418  bnj1414  32419  bnj1415  32420  bnj1421  32424  bnj1423  32433  bnj1489  32438  bnj1493  32441  bnj60  32444  bnj1500  32450  bnj1522  32454  cvmliftlem11  32655  dfon2  33150  sltsolem1  33293  brpprod3b  33461  brapply  33512  brrestrict  33523  dfrdg4  33525  cgr3permute3  33621  cgr3permute1  33622  cgr3permute2  33623  cgr3permute4  33624  cgr3permute5  33625  colinearxfr  33649  brsegle  33682  bj-prmoore  34530  bj-imdirco  34605  wl-equsal1t  34946  bicontr  35518  lub0N  36485  glb0N  36489  glbconN  36673  dalemeea  36959  dalem4  36961  dalem6  36964  dalem7  36965  dalem11  36970  dalem12  36971  dalem29  36997  dalem30  36998  dalem31N  36999  dalem32  37000  dalem33  37001  dalem34  37002  dalem35  37003  dalem36  37004  dalem37  37005  dalem40  37008  dalem46  37014  dalem47  37015  dalem49  37017  dalem50  37018  dalem52  37020  dalem53  37021  dalem54  37022  dalem56  37024  dalem58  37026  dalem59  37027  dalem62  37030  paddval  37094  4atexlemex4  37369  4atexlemex6  37370  cdleme31sdnN  37683  cdlemefr44  37721  cdleme48fv  37795  cdlemeg49lebilem  37835  cdleme50eq  37837  rngunsnply  40117  ifpbiidcor  40182  frege129d  40464  axfrege54a  40562  ismnuprim  41002  rr-grothprimbi  41003  iotaequ  41133  2uasban  41268  uunT1  41486  e2ebindVD  41618  e2ebindALT  41635  iunconnALT  41642  dfxlim2  42490  ioodvbdlimc1  42575  ioodvbdlimc2  42577  fourierdlem86  42834  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  hoidmvlelem1  43234  hoidmvlelem3  43236  hoidmvlelem4  43237  rngccatidALTV  44613  ringccatidALTV  44676