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 2761. (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  2761  abid1  2897  abid2f  2953  ceqsexg  3607  symdifass  4208  wecmpep  5643  sorpss  7742  epweon  7787  epweonALT  7788  tz7.49c  8449  dford2  9614  infxpen  10086  isacn  10116  dfac5  10200  dfackm  10238  pwfseq  10742  axgroth5  10902  axgroth6  10906  supmul  12282  elfz0lmr  13911  sgnneg  15246  fsum2d  15930  cbvprod  16075  cbvprodv  16076  fprod2d  16141  rpnnen2lem12  16386  isstruct  17323  oppccatid  17886  subccatid  18014  fuccatid  18140  setccatid  18252  catccatid  18274  estrccatid  18299  xpccatid  18355  lubfun  18517  lubeldm  18518  lubelss  18519  lubval  18521  lubcl  18522  lubprop  18523  lublecl  18526  lubid  18527  glbfun  18530  glbeldm  18531  glbelss  18532  glbval  18534  glbcl  18535  glbprop  18536  joinval2  18546  joineu  18547  meetval2  18560  meeteu  18561  join0  18570  meet0  18571  odulub  18572  oduglb  18574  poslubd  18578  isglbd  18676  lubun  18682  symgsssg  19674  symgfisg  19675  pmtr3ncomlem1  19680  opprsubg  20575  lmodvscl  21146  opsrtos  22359  iscnp2  23550  cbvditg  26167  ditgsplit  26174  lgsquad2  27706  2sqreuop  27782  2sqreuopnn  27783  2sqreuoplt  27784  2sqreuopltb  27785  2sqreuopnnlt  27786  2sqreuopnnltb  27787  ltssolem1  28025  addcuts  28357  mulcut  28511  elreno2  28874  nb3grpr  29956  clwwlkccat  30574  clwlkclwwlk  30586  clwwlknccat  30647  frgr3v  30869  eqid1  31061  grpoidinv  31103  stri  32852  hstri  32860  stcltrthi  32873  sq2reunnltb  33074  nmo  33079  elxrge02  33491  toslub  33527  tosglb  33529  xrsclat  33565  slmdvscl  33768  zarclsun  34495  unelldsys  34784  omssubadd  34925  ballotlemimin  35131  ballotlemfrcn0  35155  bnj1383  35454  bnj1386  35456  bnj153  35503  bnj543  35516  bnj544  35517  bnj546  35519  bnj605  35530  bnj579  35537  bnj600  35542  bnj601  35543  bnj852  35544  bnj893  35551  bnj906  35553  bnj917  35557  bnj938  35560  bnj944  35561  bnj998  35580  bnj1006  35583  bnj1029  35591  bnj1034  35593  bnj1124  35611  bnj1128  35613  bnj1127  35614  bnj1125  35615  bnj1147  35617  bnj1190  35631  bnj69  35633  bnj1204  35635  bnj1311  35647  bnj1318  35648  bnj1384  35655  bnj1408  35659  bnj1414  35660  bnj1415  35661  bnj1421  35665  bnj1423  35674  bnj1489  35679  bnj1493  35682  bnj60  35685  bnj1500  35691  bnj1522  35695  cvmliftlem11  36039  currybi  36432  dfon2  36534  brpprod3b  36629  brapply  36680  brrestrict  36693  dfrdg4  36695  cgr3permute3  36792  cgr3permute1  36793  cgr3permute2  36794  cgr3permute4  36795  cgr3permute5  36796  colinearxfr  36820  brsegle  36853  riotaeqi  36968  prodeq2si  36973  bj-prmoore  38016  bj-imdirco  38091  wl-equsal1t  38454  bicontr  38994  lub0N  40226  glb0N  40230  glbconN  40414  dalemeea  40700  dalem4  40702  dalem6  40705  dalem7  40706  dalem11  40711  dalem12  40712  dalem29  40738  dalem30  40739  dalem31N  40740  dalem32  40741  dalem33  40742  dalem34  40743  dalem35  40744  dalem36  40745  dalem37  40746  dalem40  40749  dalem46  40755  dalem47  40756  dalem49  40758  dalem50  40759  dalem52  40761  dalem53  40762  dalem54  40763  dalem56  40765  dalem58  40767  dalem59  40768  dalem62  40771  paddval  40835  4atexlemex4  41110  4atexlemex6  41111  cdleme31sdnN  41424  cdlemefr44  41462  cdleme48fv  41536  cdlemeg49lebilem  41576  cdleme50eq  41578  rngunsnply  44155  ifpbiidcor  44459  frege129d  44748  axfrege54a  44846  ismnuprim  45263  rr-grothprimbi  45264  iotaequ  45398  2uasban  45530  uunT1  45747  e2ebindVD  45879  e2ebindALT  45896  iunconnALT  45903  dfxlim2  46827  ioodvbdlimc1  46912  ioodvbdlimc2  46914  fourierdlem86  47171  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  hoidmvlelem1  47574  hoidmvlelem3  47576  hoidmvlelem4  47577  grtriproplem  49006  grtrif1o  49009  rngccatidALTV  49338  ringccatidALTV  49372  map0cor  49934  lubeldm2d  50035  glbeldm2d  50036  lubsscl  50037  glbsscl  50038  joindm3  50046  meetdm3  50048  isclatd  50060  ipolub00  50070  ssccatid  50149  indthinc  50539  indthincALT  50540  prsthinc  50541  mndtccatid  50664  setc1onsubc  50679  2alsraln0  50882