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  388  an21  641  3anbi1i  1156  3anbi2i  1157  3anbi3i  1158  trubitru  1568  falbifal  1571  hadcomaOLD  1601  hadcomb  1602  eqid  2738  abid1  2881  ceqsexg  3583  ralab  3628  symdifass  4186  wecmpep  5577  sorpss  7572  epweon  7616  epweonOLD  7617  tz7.49c  8265  dford2  9366  infxpen  9758  isacn  9788  dfac5  9872  dfackm  9910  pwfseq  10408  axgroth5  10568  axgroth6  10572  supmul  11935  elfz0lmr  13490  fsum2d  15471  cbvprod  15613  fprod2d  15679  rpnnen2lem12  15922  isstruct  16841  oppccatid  17418  subccatid  17549  fuccatid  17675  setccatid  17787  catccatid  17809  estrccatid  17836  xpccatid  17893  lubfun  18058  lubeldm  18059  lubelss  18060  lubval  18062  lubcl  18063  lubprop  18064  lublecl  18067  lubid  18068  glbfun  18071  glbeldm  18072  glbelss  18073  glbval  18075  glbcl  18076  glbprop  18077  joinval2  18087  joineu  18088  meetval2  18101  meeteu  18102  join0  18111  meet0  18112  odulub  18113  oduglb  18115  poslubd  18119  isglbd  18215  lubun  18221  symgsssg  19063  symgfisg  19064  pmtr3ncomlem1  19069  opprsubg  19866  abvtriv  20089  lmodvscl  20128  opsrtos  21252  iscnp2  22378  cbvditg  25006  ditgsplit  25013  lgsquad2  26522  2sqreuop  26598  2sqreuopnn  26599  2sqreuoplt  26600  2sqreuopltb  26601  2sqreuopnnlt  26602  2sqreuopnnltb  26603  nb3grpr  27737  clwwlkccat  28340  clwlkclwwlk  28352  clwwlknccat  28413  frgr3v  28625  eqid1  28817  grpoidinv  28856  stri  30605  hstri  30613  stcltrthi  30626  sq2reunnltb  30819  nmo  30824  elxrge02  31192  toslub  31237  tosglb  31239  xrsclat  31275  slmdvscl  31453  zarclsun  31806  unelldsys  32112  omssubadd  32253  ballotlemimin  32458  ballotlemfrcn0  32482  sgnneg  32493  bnj1383  32797  bnj1386  32799  bnj153  32846  bnj543  32859  bnj544  32860  bnj546  32862  bnj605  32873  bnj579  32880  bnj600  32885  bnj601  32886  bnj852  32887  bnj893  32894  bnj906  32896  bnj917  32900  bnj938  32903  bnj944  32904  bnj998  32923  bnj1006  32926  bnj1029  32934  bnj1034  32936  bnj1124  32954  bnj1128  32956  bnj1127  32957  bnj1125  32958  bnj1147  32960  bnj1190  32974  bnj69  32976  bnj1204  32978  bnj1311  32990  bnj1318  32991  bnj1384  32998  bnj1408  33002  bnj1414  33003  bnj1415  33004  bnj1421  33008  bnj1423  33017  bnj1489  33022  bnj1493  33025  bnj60  33028  bnj1500  33034  bnj1522  33038  cvmliftlem11  33243  dfon2  33754  sltsolem1  33864  brpprod3b  34175  brapply  34226  brrestrict  34237  dfrdg4  34239  cgr3permute3  34335  cgr3permute1  34336  cgr3permute2  34337  cgr3permute4  34338  cgr3permute5  34339  colinearxfr  34363  brsegle  34396  bj-prmoore  35272  bj-imdirco  35347  wl-equsal1t  35686  bicontr  36224  lub0N  37189  glb0N  37193  glbconN  37377  dalemeea  37663  dalem4  37665  dalem6  37668  dalem7  37669  dalem11  37674  dalem12  37675  dalem29  37701  dalem30  37702  dalem31N  37703  dalem32  37704  dalem33  37705  dalem34  37706  dalem35  37707  dalem36  37708  dalem37  37709  dalem40  37712  dalem46  37718  dalem47  37719  dalem49  37721  dalem50  37722  dalem52  37724  dalem53  37725  dalem54  37726  dalem56  37728  dalem58  37730  dalem59  37731  dalem62  37734  paddval  37798  4atexlemex4  38073  4atexlemex6  38074  cdleme31sdnN  38387  cdlemefr44  38425  cdleme48fv  38499  cdlemeg49lebilem  38539  cdleme50eq  38541  rngunsnply  40984  ifpbiidcor  41049  frege129d  41330  axfrege54a  41428  ismnuprim  41871  rr-grothprimbi  41872  iotaequ  42006  2uasban  42141  uunT1  42359  e2ebindVD  42491  e2ebindALT  42508  iunconnALT  42515  dfxlim2  43348  ioodvbdlimc1  43433  ioodvbdlimc2  43435  fourierdlem86  43692  fourierdlem94  43700  fourierdlem103  43709  fourierdlem104  43710  fourierdlem113  43719  hoidmvlelem1  44092  hoidmvlelem3  44094  hoidmvlelem4  44095  rngccatidALTV  45503  ringccatidALTV  45566  map0cor  46138  lubeldm2d  46208  glbeldm2d  46209  lubsscl  46210  glbsscl  46211  joindm3  46219  meetdm3  46221  isclatd  46225  ipolub00  46235  indthinc  46289  indthincALT  46290  prsthinc  46291  mndtccatid  46330