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 2760. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 212	1 ⊢ (𝜑 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biidd  265  pm5.19  391  an21  657  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  trubitru  1599  falbifal  1602  hadcomb  1630  eqid  2760  abid1  2896  abid2f  2952  ceqsexg  3607  symdifass  4208  wecmpep  5647  sorpss  7729  epweon  7774  epweonALT  7775  tz7.49c  8435  dford2  9599  infxpen  10017  isacn  10047  dfac5  10131  dfackm  10169  pwfseq  10673  axgroth5  10833  axgroth6  10837  supmul  12211  elfz0lmr  13839  sgnneg  15173  fsum2d  15857  cbvprod  16002  cbvprodv  16003  fprod2d  16068  rpnnen2lem12  16313  isstruct  17244  oppccatid  17807  subccatid  17935  fuccatid  18061  setccatid  18173  catccatid  18195  estrccatid  18220  xpccatid  18276  lubfun  18438  lubeldm  18439  lubelss  18440  lubval  18442  lubcl  18443  lubprop  18444  lublecl  18447  lubid  18448  glbfun  18451  glbeldm  18452  glbelss  18453  glbval  18455  glbcl  18456  glbprop  18457  joinval2  18467  joineu  18468  meetval2  18481  meeteu  18482  join0  18491  meet0  18492  odulub  18493  oduglb  18495  poslubd  18499  isglbd  18597  lubun  18603  symgsssg  19594  symgfisg  19595  pmtr3ncomlem1  19600  opprsubg  20493  lmodvscl  21062  opsrtos  22273  iscnp2  23464  cbvditg  26081  ditgsplit  26088  lgsquad2  27622  2sqreuop  27698  2sqreuopnn  27699  2sqreuoplt  27700  2sqreuopltb  27701  2sqreuopnnlt  27702  2sqreuopnnltb  27703  ltssolem1  27911  addcuts  28243  mulcut  28397  elreno2  28760  nb3grpr  29842  clwwlkccat  30460  clwlkclwwlk  30472  clwwlknccat  30533  frgr3v  30755  eqid1  30947  grpoidinv  30989  stri  32738  hstri  32746  stcltrthi  32759  sq2reunnltb  32960  nmo  32965  elxrge02  33377  toslub  33413  tosglb  33415  xrsclat  33451  slmdvscl  33654  zarclsun  34380  unelldsys  34669  omssubadd  34811  ballotlemimin  35017  ballotlemfrcn0  35041  bnj1383  35340  bnj1386  35342  bnj153  35389  bnj543  35402  bnj544  35403  bnj546  35405  bnj605  35416  bnj579  35423  bnj600  35428  bnj601  35429  bnj852  35430  bnj893  35437  bnj906  35439  bnj917  35443  bnj938  35446  bnj944  35447  bnj998  35466  bnj1006  35469  bnj1029  35477  bnj1034  35479  bnj1124  35497  bnj1128  35499  bnj1127  35500  bnj1125  35501  bnj1147  35503  bnj1190  35517  bnj69  35519  bnj1204  35521  bnj1311  35533  bnj1318  35534  bnj1384  35541  bnj1408  35545  bnj1414  35546  bnj1415  35547  bnj1421  35551  bnj1423  35560  bnj1489  35565  bnj1493  35568  bnj60  35571  bnj1500  35577  bnj1522  35581  cvmliftlem11  35874  currybi  36267  dfon2  36369  brpprod3b  36464  brapply  36515  brrestrict  36528  dfrdg4  36530  cgr3permute3  36627  cgr3permute1  36628  cgr3permute2  36629  cgr3permute4  36630  cgr3permute5  36631  colinearxfr  36655  brsegle  36688  riotaeqi  36819  prodeq2si  36824  bj-prmoore  37865  bj-imdirco  37942  wl-equsal1t  38305  bicontr  38830  lub0N  40062  glb0N  40066  glbconN  40250  dalemeea  40536  dalem4  40538  dalem6  40541  dalem7  40542  dalem11  40547  dalem12  40548  dalem29  40574  dalem30  40575  dalem31N  40576  dalem32  40577  dalem33  40578  dalem34  40579  dalem35  40580  dalem36  40581  dalem37  40582  dalem40  40585  dalem46  40591  dalem47  40592  dalem49  40594  dalem50  40595  dalem52  40597  dalem53  40598  dalem54  40599  dalem56  40601  dalem58  40603  dalem59  40604  dalem62  40607  paddval  40671  4atexlemex4  40946  4atexlemex6  40947  cdleme31sdnN  41260  cdlemefr44  41298  cdleme48fv  41372  cdlemeg49lebilem  41412  cdleme50eq  41414  rngunsnply  44010  ifpbiidcor  44314  frege129d  44603  axfrege54a  44701  ismnuprim  45118  rr-grothprimbi  45119  iotaequ  45253  2uasban  45385  uunT1  45602  e2ebindVD  45734  e2ebindALT  45751  iunconnALT  45758  dfxlim2  46676  ioodvbdlimc1  46761  ioodvbdlimc2  46763  fourierdlem86  47020  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem113  47047  hoidmvlelem1  47423  hoidmvlelem3  47425  hoidmvlelem4  47426  grtriproplem  48855  grtrif1o  48858  rngccatidALTV  49187  ringccatidALTV  49221  map0cor  49783  lubeldm2d  49884  glbeldm2d  49885  lubsscl  49886  glbsscl  49887  joindm3  49895  meetdm3  49897  isclatd  49909  ipolub00  49919  ssccatid  49998  indthinc  50388  indthincALT  50389  prsthinc  50390  mndtccatid  50513  setc1onsubc  50528  2alsraln0  50746