Theorem biid 253

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 2825. (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 201	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  biidd  254  pm5.19  378  3anbi1i  1200  3anbi2i  1201  3anbi3i  1202  trubitru  1686  falbifal  1689  hadcoma  1712  hadcomb  1713  eqid  2825  abid1  2949  ceqsexg  3552  symdifass  4081  wecmpep  5338  opelresgOLD2  5643  sorpss  7207  epweon  7248  tz7.49c  7812  dford2  8801  infxpen  9157  isacn  9187  dfac5  9271  dfackm  9310  pwfseq  9808  axgroth5  9968  axgroth6  9972  supmul  11332  elfz0lmr  12885  fsum2d  14884  cbvprod  15025  fprod2d  15091  rpnnen2lem12  15335  isstruct  16242  oppccatid  16738  subccatid  16865  fuccatid  16988  setccatid  17093  catccatid  17111  estrccatid  17131  xpccatid  17188  lubfun  17340  lubeldm  17341  lubelss  17342  lubval  17344  lubcl  17345  lubprop  17346  lublecl  17349  lubid  17350  glbfun  17353  glbeldm  17354  glbelss  17355  glbval  17357  glbcl  17358  glbprop  17359  joinval2  17369  joineu  17370  meetval2  17383  meeteu  17384  isglbd  17477  lubun  17483  meet0  17497  join0  17498  oduglb  17499  odulub  17501  poslubd  17508  symgsssg  18244  symgfisg  18245  pmtr3ncomlem1  18250  opprsubg  18997  abvtriv  19204  lmodvscl  19243  opsrtos  19853  iscnp2  21421  cbvditg  24024  ditgsplit  24031  lgsquad2  25531  nb3grpr  26687  clwwlkccat  27326  clwlkclwwlk  27338  clwlkclwwlkOLD  27339  clwwlknccat  27416  clwlksfclwwlkOLD  27438  frgr3v  27652  eqid1  27877  grpoidinv  27914  stri  29667  hstri  29675  stcltrthi  29688  nmo  29876  elxrge02  30181  toslub  30209  tosglb  30211  xrsclat  30221  slmdvscl  30308  unelldsys  30762  omssubadd  30903  ballotlemimin  31109  ballotlemfrcn0  31133  sgnneg  31144  bnj1383  31444  bnj1386  31446  bnj153  31492  bnj543  31505  bnj544  31506  bnj546  31508  bnj605  31519  bnj579  31526  bnj600  31531  bnj601  31532  bnj852  31533  bnj893  31540  bnj906  31542  bnj917  31546  bnj938  31549  bnj944  31550  bnj998  31568  bnj1006  31571  bnj1029  31578  bnj1034  31580  bnj1124  31598  bnj1128  31600  bnj1127  31601  bnj1125  31602  bnj1147  31604  bnj1190  31618  bnj69  31620  bnj1204  31622  bnj1311  31634  bnj1318  31635  bnj1384  31642  bnj1408  31646  bnj1414  31647  bnj1415  31648  bnj1421  31652  bnj1423  31661  bnj1489  31666  bnj1493  31669  bnj60  31672  bnj1500  31678  bnj1522  31682  cvmliftlem11  31819  dfon2  32230  sltsolem1  32360  brpprod3b  32528  brapply  32579  brrestrict  32590  dfrdg4  32592  cgr3permute3  32688  cgr3permute1  32689  cgr3permute2  32690  cgr3permute4  32691  cgr3permute5  32692  colinearxfr  32716  brsegle  32749  bj-ssbequ2  33178  bj-abid2  33304  bj-termab  33366  bj-restuni  33568  wl-equsal1t  33866  bicontr  34416  lub0N  35259  glb0N  35263  glbconN  35447  dalemeea  35733  dalem4  35735  dalem6  35738  dalem7  35739  dalem11  35744  dalem12  35745  dalem29  35771  dalem30  35772  dalem31N  35773  dalem32  35774  dalem33  35775  dalem34  35776  dalem35  35777  dalem36  35778  dalem37  35779  dalem40  35782  dalem46  35788  dalem47  35789  dalem49  35791  dalem50  35792  dalem52  35794  dalem53  35795  dalem54  35796  dalem56  35798  dalem58  35800  dalem59  35801  dalem62  35804  paddval  35868  4atexlemex4  36143  4atexlemex6  36144  cdleme31sdnN  36457  cdlemefr44  36495  cdleme48fv  36569  cdlemeg49lebilem  36609  cdleme50eq  36611  rngunsnply  38581  ifpbiidcor  38656  frege129d  38891  axfrege54a  38990  iotaequ  39464  2uasban  39601  uunT1  39829  e2ebindVD  39961  e2ebindALT  39978  iunconnALT  39985  disjinfi  40183  dfxlim2  40863  ioodvbdlimc1  40937  ioodvbdlimc2  40939  fourierdlem86  41197  fourierdlem94  41205  fourierdlem103  41214  fourierdlem104  41215  fourierdlem113  41224  hoidmvlelem1  41597  hoidmvlelem3  41599  hoidmvlelem4  41600  rngccatidALTV  42850  ringccatidALTV  42913