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 2735. (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  2735  abid1  2871  abid2f  2929  ceqsexg  3632  ralab  3676  symdifass  4237  wecmpep  5646  sorpss  7720  epweon  7767  epweonALT  7768  tz7.49c  8458  dford2  9632  infxpen  10026  isacn  10056  dfac5  10141  dfackm  10179  pwfseq  10676  axgroth5  10836  axgroth6  10840  supmul  12212  elfz0lmr  13796  fsum2d  15785  cbvprod  15927  cbvprodv  15928  fprod2d  15995  rpnnen2lem12  16241  isstruct  17169  oppccatid  17729  subccatid  17857  fuccatid  17983  setccatid  18095  catccatid  18117  estrccatid  18142  xpccatid  18198  lubfun  18360  lubeldm  18361  lubelss  18362  lubval  18364  lubcl  18365  lubprop  18366  lublecl  18369  lubid  18370  glbfun  18373  glbeldm  18374  glbelss  18375  glbval  18377  glbcl  18378  glbprop  18379  joinval2  18389  joineu  18390  meetval2  18403  meeteu  18404  join0  18413  meet0  18414  odulub  18415  oduglb  18417  poslubd  18421  isglbd  18517  lubun  18523  symgsssg  19446  symgfisg  19447  pmtr3ncomlem1  19452  opprsubg  20310  lmodvscl  20833  opsrtos  22013  iscnp2  23175  cbvditg  25805  ditgsplit  25812  lgsquad2  27347  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  sltsolem1  27637  addscut  27928  mulscut  28075  nb3grpr  29307  clwwlkccat  29917  clwlkclwwlk  29929  clwwlknccat  29990  frgr3v  30202  eqid1  30394  grpoidinv  30435  stri  32184  hstri  32192  stcltrthi  32205  sq2reunnltb  32412  nmo  32417  sgnneg  32758  elxrge02  32852  toslub  32899  tosglb  32901  xrsclat  32949  slmdvscl  33157  zarclsun  33847  unelldsys  34135  omssubadd  34278  ballotlemimin  34484  ballotlemfrcn0  34508  bnj1383  34808  bnj1386  34810  bnj153  34857  bnj543  34870  bnj544  34871  bnj546  34873  bnj605  34884  bnj579  34891  bnj600  34896  bnj601  34897  bnj852  34898  bnj893  34905  bnj906  34907  bnj917  34911  bnj938  34914  bnj944  34915  bnj998  34934  bnj1006  34937  bnj1029  34945  bnj1034  34947  bnj1124  34965  bnj1128  34967  bnj1127  34968  bnj1125  34969  bnj1147  34971  bnj1190  34985  bnj69  34987  bnj1204  34989  bnj1311  35001  bnj1318  35002  bnj1384  35009  bnj1408  35013  bnj1414  35014  bnj1415  35015  bnj1421  35019  bnj1423  35028  bnj1489  35033  bnj1493  35036  bnj60  35039  bnj1500  35045  bnj1522  35049  cvmliftlem11  35263  currybi  35656  dfon2  35756  brpprod3b  35851  brapply  35902  brrestrict  35913  dfrdg4  35915  cgr3permute3  36011  cgr3permute1  36012  cgr3permute2  36013  cgr3permute4  36014  cgr3permute5  36015  colinearxfr  36039  brsegle  36072  riotaeqi  36163  prodeq2si  36168  bj-prmoore  37079  bj-imdirco  37154  wl-equsal1t  37506  bicontr  38050  lub0N  39153  glb0N  39157  glbconN  39341  glbconNOLD  39342  dalemeea  39628  dalem4  39630  dalem6  39633  dalem7  39634  dalem11  39639  dalem12  39640  dalem29  39666  dalem30  39667  dalem31N  39668  dalem32  39669  dalem33  39670  dalem34  39671  dalem35  39672  dalem36  39673  dalem37  39674  dalem40  39677  dalem46  39683  dalem47  39684  dalem49  39686  dalem50  39687  dalem52  39689  dalem53  39690  dalem54  39691  dalem56  39693  dalem58  39695  dalem59  39696  dalem62  39699  paddval  39763  4atexlemex4  40038  4atexlemex6  40039  cdleme31sdnN  40352  cdlemefr44  40390  cdleme48fv  40464  cdlemeg49lebilem  40504  cdleme50eq  40506  rngunsnply  43140  ifpbiidcor  43445  frege129d  43734  axfrege54a  43832  ismnuprim  44266  rr-grothprimbi  44267  iotaequ  44401  2uasban  44535  uunT1  44752  e2ebindVD  44884  e2ebindALT  44901  iunconnALT  44908  dfxlim2  45825  ioodvbdlimc1  45910  ioodvbdlimc2  45912  fourierdlem86  46169  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  hoidmvlelem1  46572  hoidmvlelem3  46574  hoidmvlelem4  46575  grtriproplem  47899  grtrif1o  47902  rngccatidALTV  48195  ringccatidALTV  48229  map0cor  48781  lubeldm2d  48880  glbeldm2d  48881  lubsscl  48882  glbsscl  48883  joindm3  48891  meetdm3  48893  isclatd  48905  ipolub00  48915  ssccatid  48987  indthinc  49296  indthincALT  49297  prsthinc  49298  mndtccatid  49412  setc1onsubc  49427