Theorem biid 263

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 2823. (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 211	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  biidd  264  pm5.19  390  an21  642  3anbi1i  1153  3anbi2i  1154  3anbi3i  1155  trubitru  1566  falbifal  1569  hadcomaOLD  1600  hadcomb  1601  sb6fALT  2602  sbi2ALT  2607  sbrimALT  2609  sbanALT  2610  sbbiALT  2611  sbieALT  2613  sbiedALT  2614  sbco2ALT  2615  sb7fALT  2616  eqid  2823  abid1  2958  ceqsexg  3648  symdifass  4230  wecmpep  5549  sorpss  7456  epweon  7499  tz7.49c  8084  dford2  9085  infxpen  9442  isacn  9472  dfac5  9556  dfackm  9594  pwfseq  10088  axgroth5  10248  axgroth6  10252  supmul  11615  elfz0lmr  13155  fsum2d  15128  cbvprod  15271  fprod2d  15337  rpnnen2lem12  15580  isstruct  16498  oppccatid  16991  subccatid  17118  fuccatid  17241  setccatid  17346  catccatid  17364  estrccatid  17384  xpccatid  17440  lubfun  17592  lubeldm  17593  lubelss  17594  lubval  17596  lubcl  17597  lubprop  17598  lublecl  17601  lubid  17602  glbfun  17605  glbeldm  17606  glbelss  17607  glbval  17609  glbcl  17610  glbprop  17611  joinval2  17621  joineu  17622  meetval2  17635  meeteu  17636  isglbd  17729  lubun  17735  meet0  17749  join0  17750  oduglb  17751  odulub  17753  poslubd  17760  symgsssg  18597  symgfisg  18598  pmtr3ncomlem1  18603  opprsubg  19388  abvtriv  19614  lmodvscl  19653  opsrtos  20268  iscnp2  21849  cbvditg  24454  ditgsplit  24461  lgsquad2  25964  2sqreuop  26040  2sqreuopnn  26041  2sqreuoplt  26042  2sqreuopltb  26043  2sqreuopnnlt  26044  2sqreuopnnltb  26045  nb3grpr  27166  clwwlkccat  27770  clwlkclwwlk  27782  clwwlknccat  27844  frgr3v  28056  eqid1  28248  grpoidinv  28287  stri  30036  hstri  30044  stcltrthi  30057  sq2reunnltb  30250  nmo  30256  elxrge02  30610  toslub  30657  tosglb  30659  xrsclat  30669  slmdvscl  30844  unelldsys  31419  omssubadd  31560  ballotlemimin  31765  ballotlemfrcn0  31789  sgnneg  31800  bnj1383  32105  bnj1386  32107  bnj153  32154  bnj543  32167  bnj544  32168  bnj546  32170  bnj605  32181  bnj579  32188  bnj600  32193  bnj601  32194  bnj852  32195  bnj893  32202  bnj906  32204  bnj917  32208  bnj938  32211  bnj944  32212  bnj998  32231  bnj1006  32234  bnj1029  32242  bnj1034  32244  bnj1124  32262  bnj1128  32264  bnj1127  32265  bnj1125  32266  bnj1147  32268  bnj1190  32282  bnj69  32284  bnj1204  32286  bnj1311  32298  bnj1318  32299  bnj1384  32306  bnj1408  32310  bnj1414  32311  bnj1415  32312  bnj1421  32316  bnj1423  32325  bnj1489  32330  bnj1493  32333  bnj60  32336  bnj1500  32342  bnj1522  32346  cvmliftlem11  32544  dfon2  33039  sltsolem1  33182  brpprod3b  33350  brapply  33401  brrestrict  33412  dfrdg4  33414  cgr3permute3  33510  cgr3permute1  33511  cgr3permute2  33512  cgr3permute4  33513  cgr3permute5  33514  colinearxfr  33538  brsegle  33571  bj-prmoore  34409  wl-equsal1t  34783  bicontr  35360  lub0N  36327  glb0N  36331  glbconN  36515  dalemeea  36801  dalem4  36803  dalem6  36806  dalem7  36807  dalem11  36812  dalem12  36813  dalem29  36839  dalem30  36840  dalem31N  36841  dalem32  36842  dalem33  36843  dalem34  36844  dalem35  36845  dalem36  36846  dalem37  36847  dalem40  36850  dalem46  36856  dalem47  36857  dalem49  36859  dalem50  36860  dalem52  36862  dalem53  36863  dalem54  36864  dalem56  36866  dalem58  36868  dalem59  36869  dalem62  36872  paddval  36936  4atexlemex4  37211  4atexlemex6  37212  cdleme31sdnN  37525  cdlemefr44  37563  cdleme48fv  37637  cdlemeg49lebilem  37677  cdleme50eq  37679  rngunsnply  39780  ifpbiidcor  39847  frege129d  40115  axfrege54a  40214  ismnuprim  40637  rr-grothprimbi  40638  iotaequ  40768  2uasban  40903  uunT1  41121  e2ebindVD  41253  e2ebindALT  41270  iunconnALT  41277  disjinfi  41461  dfxlim2  42136  ioodvbdlimc1  42225  ioodvbdlimc2  42227  fourierdlem86  42484  fourierdlem94  42492  fourierdlem103  42501  fourierdlem104  42502  fourierdlem113  42511  hoidmvlelem1  42884  hoidmvlelem3  42886  hoidmvlelem4  42887  rngccatidALTV  44267  ringccatidALTV  44330