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 2728. (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  262  pm5.19  386  an21  643  3anbi1i  1155  3anbi2i  1156  3anbi3i  1157  trubitru  1563  falbifal  1566  hadcomb  1594  eqid  2728  abid1  2866  abid2f  2933  ceqsexg  3639  ralab  3686  symdifass  4252  wecmpep  5670  sorpss  7733  epweon  7777  epweonALT  7778  tz7.49c  8467  dford2  9644  infxpen  10038  isacn  10068  dfac5  10152  dfackm  10190  pwfseq  10688  axgroth5  10848  axgroth6  10852  supmul  12217  elfz0lmr  13780  fsum2d  15750  cbvprod  15892  fprod2d  15958  rpnnen2lem12  16202  isstruct  17121  oppccatid  17701  subccatid  17832  fuccatid  17961  setccatid  18073  catccatid  18095  estrccatid  18122  xpccatid  18179  lubfun  18344  lubeldm  18345  lubelss  18346  lubval  18348  lubcl  18349  lubprop  18350  lublecl  18353  lubid  18354  glbfun  18357  glbeldm  18358  glbelss  18359  glbval  18361  glbcl  18362  glbprop  18363  joinval2  18373  joineu  18374  meetval2  18387  meeteu  18388  join0  18397  meet0  18398  odulub  18399  oduglb  18401  poslubd  18405  isglbd  18501  lubun  18507  symgsssg  19422  symgfisg  19423  pmtr3ncomlem1  19428  opprsubg  20291  abvtriv  20721  lmodvscl  20761  opsrtos  22001  iscnp2  23156  cbvditg  25796  ditgsplit  25803  lgsquad2  27332  2sqreuop  27408  2sqreuopnn  27409  2sqreuoplt  27410  2sqreuopltb  27411  2sqreuopnnlt  27412  2sqreuopnnltb  27413  sltsolem1  27621  addscut  27908  mulscut  28045  nb3grpr  29208  clwwlkccat  29813  clwlkclwwlk  29825  clwwlknccat  29886  frgr3v  30098  eqid1  30290  grpoidinv  30331  stri  32080  hstri  32088  stcltrthi  32101  sq2reunnltb  32296  nmo  32301  elxrge02  32668  toslub  32713  tosglb  32715  xrsclat  32751  slmdvscl  32934  zarclsun  33471  unelldsys  33777  omssubadd  33920  ballotlemimin  34125  ballotlemfrcn0  34149  sgnneg  34160  bnj1383  34462  bnj1386  34464  bnj153  34511  bnj543  34524  bnj544  34525  bnj546  34527  bnj605  34538  bnj579  34545  bnj600  34550  bnj601  34551  bnj852  34552  bnj893  34559  bnj906  34561  bnj917  34565  bnj938  34568  bnj944  34569  bnj998  34588  bnj1006  34591  bnj1029  34599  bnj1034  34601  bnj1124  34619  bnj1128  34621  bnj1127  34622  bnj1125  34623  bnj1147  34625  bnj1190  34639  bnj69  34641  bnj1204  34643  bnj1311  34655  bnj1318  34656  bnj1384  34663  bnj1408  34667  bnj1414  34668  bnj1415  34669  bnj1421  34673  bnj1423  34682  bnj1489  34687  bnj1493  34690  bnj60  34693  bnj1500  34699  bnj1522  34703  cvmliftlem11  34905  currybi  35288  dfon2  35388  brpprod3b  35483  brapply  35534  brrestrict  35545  dfrdg4  35547  cgr3permute3  35643  cgr3permute1  35644  cgr3permute2  35645  cgr3permute4  35646  cgr3permute5  35647  colinearxfr  35671  brsegle  35704  bj-prmoore  36594  bj-imdirco  36669  wl-equsal1t  37009  bicontr  37553  lub0N  38661  glb0N  38665  glbconN  38849  glbconNOLD  38850  dalemeea  39136  dalem4  39138  dalem6  39141  dalem7  39142  dalem11  39147  dalem12  39148  dalem29  39174  dalem30  39175  dalem31N  39176  dalem32  39177  dalem33  39178  dalem34  39179  dalem35  39180  dalem36  39181  dalem37  39182  dalem40  39185  dalem46  39191  dalem47  39192  dalem49  39194  dalem50  39195  dalem52  39197  dalem53  39198  dalem54  39199  dalem56  39201  dalem58  39203  dalem59  39204  dalem62  39207  paddval  39271  4atexlemex4  39546  4atexlemex6  39547  cdleme31sdnN  39860  cdlemefr44  39898  cdleme48fv  39972  cdlemeg49lebilem  40012  cdleme50eq  40014  rngunsnply  42597  ifpbiidcor  42904  frege129d  43193  axfrege54a  43291  ismnuprim  43731  rr-grothprimbi  43732  iotaequ  43866  2uasban  44001  uunT1  44219  e2ebindVD  44351  e2ebindALT  44368  iunconnALT  44375  dfxlim2  45236  ioodvbdlimc1  45321  ioodvbdlimc2  45323  fourierdlem86  45580  fourierdlem94  45588  fourierdlem103  45597  fourierdlem104  45598  fourierdlem113  45607  hoidmvlelem1  45983  hoidmvlelem3  45985  hoidmvlelem4  45986  rngccatidALTV  47334  ringccatidALTV  47368  map0cor  47907  lubeldm2d  47977  glbeldm2d  47978  lubsscl  47979  glbsscl  47980  joindm3  47988  meetdm3  47990  isclatd  47994  ipolub00  48004  indthinc  48058  indthincALT  48059  prsthinc  48060  mndtccatid  48099