Theorem biid 260

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 2738. (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 208	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biidd  261  pm5.19  387  an21  640  3anbi1i  1155  3anbi2i  1156  3anbi3i  1157  trubitru  1568  falbifal  1571  hadcomaOLD  1602  hadcomb  1603  eqid  2738  abid1  2880  ceqsexg  3575  ralab  3621  symdifass  4182  wecmpep  5572  sorpss  7559  epweon  7603  tz7.49c  8247  dford2  9308  infxpen  9701  isacn  9731  dfac5  9815  dfackm  9853  pwfseq  10351  axgroth5  10511  axgroth6  10515  supmul  11877  elfz0lmr  13430  fsum2d  15411  cbvprod  15553  fprod2d  15619  rpnnen2lem12  15862  isstruct  16781  oppccatid  17347  subccatid  17477  fuccatid  17603  setccatid  17715  catccatid  17737  estrccatid  17764  xpccatid  17821  lubfun  17985  lubeldm  17986  lubelss  17987  lubval  17989  lubcl  17990  lubprop  17991  lublecl  17994  lubid  17995  glbfun  17998  glbeldm  17999  glbelss  18000  glbval  18002  glbcl  18003  glbprop  18004  joinval2  18014  joineu  18015  meetval2  18028  meeteu  18029  join0  18038  meet0  18039  odulub  18040  oduglb  18042  poslubd  18046  isglbd  18142  lubun  18148  symgsssg  18990  symgfisg  18991  pmtr3ncomlem1  18996  opprsubg  19793  abvtriv  20016  lmodvscl  20055  opsrtos  21174  iscnp2  22298  cbvditg  24923  ditgsplit  24930  lgsquad2  26439  2sqreuop  26515  2sqreuopnn  26516  2sqreuoplt  26517  2sqreuopltb  26518  2sqreuopnnlt  26519  2sqreuopnnltb  26520  nb3grpr  27652  clwwlkccat  28255  clwlkclwwlk  28267  clwwlknccat  28328  frgr3v  28540  eqid1  28732  grpoidinv  28771  stri  30520  hstri  30528  stcltrthi  30541  sq2reunnltb  30734  nmo  30739  elxrge02  31108  toslub  31153  tosglb  31155  xrsclat  31191  slmdvscl  31369  zarclsun  31722  unelldsys  32026  omssubadd  32167  ballotlemimin  32372  ballotlemfrcn0  32396  sgnneg  32407  bnj1383  32711  bnj1386  32713  bnj153  32760  bnj543  32773  bnj544  32774  bnj546  32776  bnj605  32787  bnj579  32794  bnj600  32799  bnj601  32800  bnj852  32801  bnj893  32808  bnj906  32810  bnj917  32814  bnj938  32817  bnj944  32818  bnj998  32837  bnj1006  32840  bnj1029  32848  bnj1034  32850  bnj1124  32868  bnj1128  32870  bnj1127  32871  bnj1125  32872  bnj1147  32874  bnj1190  32888  bnj69  32890  bnj1204  32892  bnj1311  32904  bnj1318  32905  bnj1384  32912  bnj1408  32916  bnj1414  32917  bnj1415  32918  bnj1421  32922  bnj1423  32931  bnj1489  32936  bnj1493  32939  bnj60  32942  bnj1500  32948  bnj1522  32952  cvmliftlem11  33157  dfon2  33674  sltsolem1  33805  brpprod3b  34116  brapply  34167  brrestrict  34178  dfrdg4  34180  cgr3permute3  34276  cgr3permute1  34277  cgr3permute2  34278  cgr3permute4  34279  cgr3permute5  34280  colinearxfr  34304  brsegle  34337  bj-prmoore  35213  bj-imdirco  35288  wl-equsal1t  35627  bicontr  36165  lub0N  37130  glb0N  37134  glbconN  37318  dalemeea  37604  dalem4  37606  dalem6  37609  dalem7  37610  dalem11  37615  dalem12  37616  dalem29  37642  dalem30  37643  dalem31N  37644  dalem32  37645  dalem33  37646  dalem34  37647  dalem35  37648  dalem36  37649  dalem37  37650  dalem40  37653  dalem46  37659  dalem47  37660  dalem49  37662  dalem50  37663  dalem52  37665  dalem53  37666  dalem54  37667  dalem56  37669  dalem58  37671  dalem59  37672  dalem62  37675  paddval  37739  4atexlemex4  38014  4atexlemex6  38015  cdleme31sdnN  38328  cdlemefr44  38366  cdleme48fv  38440  cdlemeg49lebilem  38480  cdleme50eq  38482  rngunsnply  40914  ifpbiidcor  40979  frege129d  41260  axfrege54a  41358  ismnuprim  41801  rr-grothprimbi  41802  iotaequ  41936  2uasban  42071  uunT1  42289  e2ebindVD  42421  e2ebindALT  42438  iunconnALT  42445  dfxlim2  43279  ioodvbdlimc1  43364  ioodvbdlimc2  43366  fourierdlem86  43623  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  hoidmvlelem1  44023  hoidmvlelem3  44025  hoidmvlelem4  44026  rngccatidALTV  45435  ringccatidALTV  45498  map0cor  46070  lubeldm2d  46140  glbeldm2d  46141  lubsscl  46142  glbsscl  46143  joindm3  46151  meetdm3  46153  isclatd  46157  ipolub00  46167  indthinc  46221  indthincALT  46222  prsthinc  46223  mndtccatid  46260