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 2730. (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  2730  abid1  2865  abid2f  2923  ceqsexg  3622  ralab  3667  symdifass  4228  wecmpep  5633  sorpss  7707  epweon  7754  epweonALT  7755  tz7.49c  8417  dford2  9580  infxpen  9974  isacn  10004  dfac5  10089  dfackm  10127  pwfseq  10624  axgroth5  10784  axgroth6  10788  supmul  12162  elfz0lmr  13750  fsum2d  15744  cbvprod  15886  cbvprodv  15887  fprod2d  15954  rpnnen2lem12  16200  isstruct  17129  oppccatid  17687  subccatid  17815  fuccatid  17941  setccatid  18053  catccatid  18075  estrccatid  18100  xpccatid  18156  lubfun  18318  lubeldm  18319  lubelss  18320  lubval  18322  lubcl  18323  lubprop  18324  lublecl  18327  lubid  18328  glbfun  18331  glbeldm  18332  glbelss  18333  glbval  18335  glbcl  18336  glbprop  18337  joinval2  18347  joineu  18348  meetval2  18361  meeteu  18362  join0  18371  meet0  18372  odulub  18373  oduglb  18375  poslubd  18379  isglbd  18475  lubun  18481  symgsssg  19404  symgfisg  19405  pmtr3ncomlem1  19410  opprsubg  20268  lmodvscl  20791  opsrtos  21971  iscnp2  23133  cbvditg  25762  ditgsplit  25769  lgsquad2  27304  2sqreuop  27380  2sqreuopnn  27381  2sqreuoplt  27382  2sqreuopltb  27383  2sqreuopnnlt  27384  2sqreuopnnltb  27385  sltsolem1  27594  addscut  27892  mulscut  28042  nb3grpr  29316  clwwlkccat  29926  clwlkclwwlk  29938  clwwlknccat  29999  frgr3v  30211  eqid1  30403  grpoidinv  30444  stri  32193  hstri  32201  stcltrthi  32214  sq2reunnltb  32421  nmo  32426  sgnneg  32765  elxrge02  32859  toslub  32906  tosglb  32908  xrsclat  32956  slmdvscl  33174  zarclsun  33867  unelldsys  34155  omssubadd  34298  ballotlemimin  34504  ballotlemfrcn0  34528  bnj1383  34828  bnj1386  34830  bnj153  34877  bnj543  34890  bnj544  34891  bnj546  34893  bnj605  34904  bnj579  34911  bnj600  34916  bnj601  34917  bnj852  34918  bnj893  34925  bnj906  34927  bnj917  34931  bnj938  34934  bnj944  34935  bnj998  34954  bnj1006  34957  bnj1029  34965  bnj1034  34967  bnj1124  34985  bnj1128  34987  bnj1127  34988  bnj1125  34989  bnj1147  34991  bnj1190  35005  bnj69  35007  bnj1204  35009  bnj1311  35021  bnj1318  35022  bnj1384  35029  bnj1408  35033  bnj1414  35034  bnj1415  35035  bnj1421  35039  bnj1423  35048  bnj1489  35053  bnj1493  35056  bnj60  35059  bnj1500  35065  bnj1522  35069  cvmliftlem11  35289  currybi  35682  dfon2  35787  brpprod3b  35882  brapply  35933  brrestrict  35944  dfrdg4  35946  cgr3permute3  36042  cgr3permute1  36043  cgr3permute2  36044  cgr3permute4  36045  cgr3permute5  36046  colinearxfr  36070  brsegle  36103  riotaeqi  36194  prodeq2si  36199  bj-prmoore  37110  bj-imdirco  37185  wl-equsal1t  37537  bicontr  38081  lub0N  39189  glb0N  39193  glbconN  39377  glbconNOLD  39378  dalemeea  39664  dalem4  39666  dalem6  39669  dalem7  39670  dalem11  39675  dalem12  39676  dalem29  39702  dalem30  39703  dalem31N  39704  dalem32  39705  dalem33  39706  dalem34  39707  dalem35  39708  dalem36  39709  dalem37  39710  dalem40  39713  dalem46  39719  dalem47  39720  dalem49  39722  dalem50  39723  dalem52  39725  dalem53  39726  dalem54  39727  dalem56  39729  dalem58  39731  dalem59  39732  dalem62  39735  paddval  39799  4atexlemex4  40074  4atexlemex6  40075  cdleme31sdnN  40388  cdlemefr44  40426  cdleme48fv  40500  cdlemeg49lebilem  40540  cdleme50eq  40542  rngunsnply  43165  ifpbiidcor  43470  frege129d  43759  axfrege54a  43857  ismnuprim  44290  rr-grothprimbi  44291  iotaequ  44425  2uasban  44559  uunT1  44776  e2ebindVD  44908  e2ebindALT  44925  iunconnALT  44932  dfxlim2  45853  ioodvbdlimc1  45938  ioodvbdlimc2  45940  fourierdlem86  46197  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  hoidmvlelem1  46600  hoidmvlelem3  46602  hoidmvlelem4  46603  grtriproplem  47942  grtrif1o  47945  rngccatidALTV  48264  ringccatidALTV  48298  map0cor  48847  lubeldm2d  48950  glbeldm2d  48951  lubsscl  48952  glbsscl  48953  joindm3  48961  meetdm3  48963  isclatd  48975  ipolub00  48985  ssccatid  49065  indthinc  49455  indthincALT  49456  prsthinc  49457  mndtccatid  49580  setc1onsubc  49595