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 2729. (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  2729  abid1  2864  abid2f  2922  ceqsexg  3616  ralab  3661  symdifass  4221  wecmpep  5623  sorpss  7684  epweon  7731  epweonALT  7732  tz7.49c  8391  dford2  9549  infxpen  9943  isacn  9973  dfac5  10058  dfackm  10096  pwfseq  10593  axgroth5  10753  axgroth6  10757  supmul  12131  elfz0lmr  13719  fsum2d  15713  cbvprod  15855  cbvprodv  15856  fprod2d  15923  rpnnen2lem12  16169  isstruct  17098  oppccatid  17656  subccatid  17784  fuccatid  17910  setccatid  18022  catccatid  18044  estrccatid  18069  xpccatid  18125  lubfun  18287  lubeldm  18288  lubelss  18289  lubval  18291  lubcl  18292  lubprop  18293  lublecl  18296  lubid  18297  glbfun  18300  glbeldm  18301  glbelss  18302  glbval  18304  glbcl  18305  glbprop  18306  joinval2  18316  joineu  18317  meetval2  18330  meeteu  18331  join0  18340  meet0  18341  odulub  18342  oduglb  18344  poslubd  18348  isglbd  18444  lubun  18450  symgsssg  19373  symgfisg  19374  pmtr3ncomlem1  19379  opprsubg  20237  lmodvscl  20760  opsrtos  21940  iscnp2  23102  cbvditg  25731  ditgsplit  25738  lgsquad2  27273  2sqreuop  27349  2sqreuopnn  27350  2sqreuoplt  27351  2sqreuopltb  27352  2sqreuopnnlt  27353  2sqreuopnnltb  27354  sltsolem1  27563  addscut  27861  mulscut  28011  nb3grpr  29285  clwwlkccat  29892  clwlkclwwlk  29904  clwwlknccat  29965  frgr3v  30177  eqid1  30369  grpoidinv  30410  stri  32159  hstri  32167  stcltrthi  32180  sq2reunnltb  32387  nmo  32392  sgnneg  32731  elxrge02  32825  toslub  32872  tosglb  32874  xrsclat  32922  slmdvscl  33140  zarclsun  33833  unelldsys  34121  omssubadd  34264  ballotlemimin  34470  ballotlemfrcn0  34494  bnj1383  34794  bnj1386  34796  bnj153  34843  bnj543  34856  bnj544  34857  bnj546  34859  bnj605  34870  bnj579  34877  bnj600  34882  bnj601  34883  bnj852  34884  bnj893  34891  bnj906  34893  bnj917  34897  bnj938  34900  bnj944  34901  bnj998  34920  bnj1006  34923  bnj1029  34931  bnj1034  34933  bnj1124  34951  bnj1128  34953  bnj1127  34954  bnj1125  34955  bnj1147  34957  bnj1190  34971  bnj69  34973  bnj1204  34975  bnj1311  34987  bnj1318  34988  bnj1384  34995  bnj1408  34999  bnj1414  35000  bnj1415  35001  bnj1421  35005  bnj1423  35014  bnj1489  35019  bnj1493  35022  bnj60  35025  bnj1500  35031  bnj1522  35035  cvmliftlem11  35255  currybi  35648  dfon2  35753  brpprod3b  35848  brapply  35899  brrestrict  35910  dfrdg4  35912  cgr3permute3  36008  cgr3permute1  36009  cgr3permute2  36010  cgr3permute4  36011  cgr3permute5  36012  colinearxfr  36036  brsegle  36069  riotaeqi  36160  prodeq2si  36165  bj-prmoore  37076  bj-imdirco  37151  wl-equsal1t  37503  bicontr  38047  lub0N  39155  glb0N  39159  glbconN  39343  glbconNOLD  39344  dalemeea  39630  dalem4  39632  dalem6  39635  dalem7  39636  dalem11  39641  dalem12  39642  dalem29  39668  dalem30  39669  dalem31N  39670  dalem32  39671  dalem33  39672  dalem34  39673  dalem35  39674  dalem36  39675  dalem37  39676  dalem40  39679  dalem46  39685  dalem47  39686  dalem49  39688  dalem50  39689  dalem52  39691  dalem53  39692  dalem54  39693  dalem56  39695  dalem58  39697  dalem59  39698  dalem62  39701  paddval  39765  4atexlemex4  40040  4atexlemex6  40041  cdleme31sdnN  40354  cdlemefr44  40392  cdleme48fv  40466  cdlemeg49lebilem  40506  cdleme50eq  40508  rngunsnply  43131  ifpbiidcor  43436  frege129d  43725  axfrege54a  43823  ismnuprim  44256  rr-grothprimbi  44257  iotaequ  44391  2uasban  44525  uunT1  44742  e2ebindVD  44874  e2ebindALT  44891  iunconnALT  44898  dfxlim2  45819  ioodvbdlimc1  45904  ioodvbdlimc2  45906  fourierdlem86  46163  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  hoidmvlelem1  46566  hoidmvlelem3  46568  hoidmvlelem4  46569  grtriproplem  47911  grtrif1o  47914  rngccatidALTV  48233  ringccatidALTV  48267  map0cor  48816  lubeldm2d  48919  glbeldm2d  48920  lubsscl  48921  glbsscl  48922  joindm3  48930  meetdm3  48932  isclatd  48944  ipolub00  48954  ssccatid  49034  indthinc  49424  indthincALT  49425  prsthinc  49426  mndtccatid  49549  setc1onsubc  49564