Theorem biid 264

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 2769. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 212	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biidd  265  pm5.19  390  an21  656  3anbi1i  1173  3anbi2i  1174  3anbi3i  1175  trubitru  1596  falbifal  1599  hadcomb  1627  eqid  2769  abid1  2905  abid2f  2961  ceqsexg  3621  symdifass  4223  wecmpep  5654  sorpss  7726  epweon  7773  epweonALT  7774  tz7.49c  8432  dford2  9588  infxpen  9997  isacn  10027  dfac5  10111  dfackm  10149  pwfseq  10648  axgroth5  10808  axgroth6  10812  supmul  12186  elfz0lmr  13811  sgnneg  15136  fsum2d  15821  cbvprod  15966  cbvprodv  15967  fprod2d  16034  rpnnen2lem12  16280  isstruct  17211  oppccatid  17774  subccatid  17902  fuccatid  18028  setccatid  18140  catccatid  18162  estrccatid  18187  xpccatid  18243  lubfun  18405  lubeldm  18406  lubelss  18407  lubval  18409  lubcl  18410  lubprop  18411  lublecl  18414  lubid  18415  glbfun  18418  glbeldm  18419  glbelss  18420  glbval  18422  glbcl  18423  glbprop  18424  joinval2  18434  joineu  18435  meetval2  18448  meeteu  18449  join0  18458  meet0  18459  odulub  18460  oduglb  18462  poslubd  18466  isglbd  18564  lubun  18570  symgsssg  19536  symgfisg  19537  pmtr3ncomlem1  19542  opprsubg  20433  lmodvscl  20976  opsrtos  22176  iscnp2  23364  cbvditg  25981  ditgsplit  25988  lgsquad2  27515  2sqreuop  27591  2sqreuopnn  27592  2sqreuoplt  27593  2sqreuopltb  27594  2sqreuopnnlt  27595  2sqreuopnnltb  27596  ltssolem1  27804  addcuts  28136  mulcut  28290  elreno2  28653  nb3grpr  29672  clwwlkccat  30281  clwlkclwwlk  30293  clwwlknccat  30354  frgr3v  30566  eqid1  30758  grpoidinv  30800  stri  32549  hstri  32557  stcltrthi  32570  sq2reunnltb  32771  nmo  32776  elxrge02  33191  toslub  33233  tosglb  33235  xrsclat  33271  slmdvscl  33474  zarclsun  34204  unelldsys  34492  omssubadd  34634  ballotlemimin  34840  ballotlemfrcn0  34864  bnj1383  35163  bnj1386  35165  bnj153  35212  bnj543  35225  bnj544  35226  bnj546  35228  bnj605  35239  bnj579  35246  bnj600  35251  bnj601  35252  bnj852  35253  bnj893  35260  bnj906  35262  bnj917  35266  bnj938  35269  bnj944  35270  bnj998  35289  bnj1006  35292  bnj1029  35300  bnj1034  35302  bnj1124  35320  bnj1128  35322  bnj1127  35323  bnj1125  35324  bnj1147  35326  bnj1190  35340  bnj69  35342  bnj1204  35344  bnj1311  35356  bnj1318  35357  bnj1384  35364  bnj1408  35368  bnj1414  35369  bnj1415  35370  bnj1421  35374  bnj1423  35383  bnj1489  35388  bnj1493  35391  bnj60  35394  bnj1500  35400  bnj1522  35404  cvmliftlem11  35685  currybi  36078  dfon2  36180  brpprod3b  36275  brapply  36326  brrestrict  36339  dfrdg4  36341  cgr3permute3  36437  cgr3permute1  36438  cgr3permute2  36439  cgr3permute4  36440  cgr3permute5  36441  colinearxfr  36465  brsegle  36498  riotaeqi  36599  prodeq2si  36604  bj-prmoore  37644  bj-imdirco  37721  wl-equsal1t  38084  bicontr  38618  lub0N  39852  glb0N  39856  glbconN  40040  dalemeea  40326  dalem4  40328  dalem6  40331  dalem7  40332  dalem11  40337  dalem12  40338  dalem29  40364  dalem30  40365  dalem31N  40366  dalem32  40367  dalem33  40368  dalem34  40369  dalem35  40370  dalem36  40371  dalem37  40372  dalem40  40375  dalem46  40381  dalem47  40382  dalem49  40384  dalem50  40385  dalem52  40387  dalem53  40388  dalem54  40389  dalem56  40391  dalem58  40393  dalem59  40394  dalem62  40397  paddval  40461  4atexlemex4  40736  4atexlemex6  40737  cdleme31sdnN  41050  cdlemefr44  41088  cdleme48fv  41162  cdlemeg49lebilem  41202  cdleme50eq  41204  rngunsnply  43787  ifpbiidcor  44091  frege129d  44380  axfrege54a  44478  ismnuprim  44895  rr-grothprimbi  44896  iotaequ  45030  2uasban  45162  uunT1  45379  e2ebindVD  45511  e2ebindALT  45528  iunconnALT  45535  dfxlim2  46453  ioodvbdlimc1  46538  ioodvbdlimc2  46540  fourierdlem86  46797  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem113  46824  hoidmvlelem1  47200  hoidmvlelem3  47202  hoidmvlelem4  47203  grtriproplem  48592  grtrif1o  48595  rngccatidALTV  48925  ringccatidALTV  48959  map0cor  49517  lubeldm2d  49620  glbeldm2d  49621  lubsscl  49622  glbsscl  49623  joindm3  49631  meetdm3  49633  isclatd  49645  ipolub00  49655  ssccatid  49734  indthinc  50124  indthincALT  50125  prsthinc  50126  mndtccatid  50249  setc1onsubc  50264