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 2736. (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  645  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  trubitru  1571  falbifal  1574  hadcomb  1602  eqid  2736  abid1  2872  abid2f  2929  ceqsexg  3595  symdifass  4202  wecmpep  5623  sorpss  7682  epweon  7729  epweonALT  7730  tz7.49c  8385  dford2  9541  infxpen  9936  isacn  9966  dfac5  10051  dfackm  10089  pwfseq  10587  axgroth5  10747  axgroth6  10751  supmul  12128  elfz0lmr  13738  fsum2d  15733  cbvprod  15878  cbvprodv  15879  fprod2d  15946  rpnnen2lem12  16192  isstruct  17122  oppccatid  17685  subccatid  17813  fuccatid  17939  setccatid  18051  catccatid  18073  estrccatid  18098  xpccatid  18154  lubfun  18316  lubeldm  18317  lubelss  18318  lubval  18320  lubcl  18321  lubprop  18322  lublecl  18325  lubid  18326  glbfun  18329  glbeldm  18330  glbelss  18331  glbval  18333  glbcl  18334  glbprop  18335  joinval2  18345  joineu  18346  meetval2  18359  meeteu  18360  join0  18369  meet0  18370  odulub  18371  oduglb  18373  poslubd  18377  isglbd  18475  lubun  18481  symgsssg  19442  symgfisg  19443  pmtr3ncomlem1  19448  opprsubg  20332  lmodvscl  20873  opsrtos  22035  iscnp2  23204  cbvditg  25821  ditgsplit  25828  lgsquad2  27349  2sqreuop  27425  2sqreuopnn  27426  2sqreuoplt  27427  2sqreuopltb  27428  2sqreuopnnlt  27429  2sqreuopnnltb  27430  ltssolem1  27639  addcuts  27970  mulcut  28124  elreno2  28487  nb3grpr  29451  clwwlkccat  30060  clwlkclwwlk  30072  clwwlknccat  30133  frgr3v  30345  eqid1  30537  grpoidinv  30579  stri  32328  hstri  32336  stcltrthi  32349  sq2reunnltb  32554  nmo  32559  sgnneg  32906  elxrge02  32991  toslub  33033  tosglb  33035  xrsclat  33071  slmdvscl  33275  zarclsun  34014  unelldsys  34302  omssubadd  34444  ballotlemimin  34650  ballotlemfrcn0  34674  bnj1383  34973  bnj1386  34975  bnj153  35022  bnj543  35035  bnj544  35036  bnj546  35038  bnj605  35049  bnj579  35056  bnj600  35061  bnj601  35062  bnj852  35063  bnj893  35070  bnj906  35072  bnj917  35076  bnj938  35079  bnj944  35080  bnj998  35099  bnj1006  35102  bnj1029  35110  bnj1034  35112  bnj1124  35130  bnj1128  35132  bnj1127  35133  bnj1125  35134  bnj1147  35136  bnj1190  35150  bnj69  35152  bnj1204  35154  bnj1311  35166  bnj1318  35167  bnj1384  35174  bnj1408  35178  bnj1414  35179  bnj1415  35180  bnj1421  35184  bnj1423  35193  bnj1489  35198  bnj1493  35201  bnj60  35204  bnj1500  35210  bnj1522  35214  cvmliftlem11  35477  currybi  35870  dfon2  35972  brpprod3b  36067  brapply  36118  brrestrict  36131  dfrdg4  36133  cgr3permute3  36229  cgr3permute1  36230  cgr3permute2  36231  cgr3permute4  36232  cgr3permute5  36233  colinearxfr  36257  brsegle  36290  riotaeqi  36381  prodeq2si  36386  bj-prmoore  37427  bj-imdirco  37504  wl-equsal1t  37867  bicontr  38401  lub0N  39635  glb0N  39639  glbconN  39823  dalemeea  40109  dalem4  40111  dalem6  40114  dalem7  40115  dalem11  40120  dalem12  40121  dalem29  40147  dalem30  40148  dalem31N  40149  dalem32  40150  dalem33  40151  dalem34  40152  dalem35  40153  dalem36  40154  dalem37  40155  dalem40  40158  dalem46  40164  dalem47  40165  dalem49  40167  dalem50  40168  dalem52  40170  dalem53  40171  dalem54  40172  dalem56  40174  dalem58  40176  dalem59  40177  dalem62  40180  paddval  40244  4atexlemex4  40519  4atexlemex6  40520  cdleme31sdnN  40833  cdlemefr44  40871  cdleme48fv  40945  cdlemeg49lebilem  40985  cdleme50eq  40987  rngunsnply  43597  ifpbiidcor  43901  frege129d  44190  axfrege54a  44288  ismnuprim  44721  rr-grothprimbi  44722  iotaequ  44856  2uasban  44989  uunT1  45206  e2ebindVD  45338  e2ebindALT  45355  iunconnALT  45362  dfxlim2  46276  ioodvbdlimc1  46361  ioodvbdlimc2  46363  fourierdlem86  46620  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  hoidmvlelem1  47023  hoidmvlelem3  47025  hoidmvlelem4  47026  grtriproplem  48415  grtrif1o  48418  rngccatidALTV  48748  ringccatidALTV  48782  map0cor  49330  lubeldm2d  49433  glbeldm2d  49434  lubsscl  49435  glbsscl  49436  joindm3  49444  meetdm3  49446  isclatd  49458  ipolub00  49468  ssccatid  49547  indthinc  49937  indthincALT  49938  prsthinc  49939  mndtccatid  50062  setc1onsubc  50077