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 2737. (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  2737  abid1  2873  abid2f  2930  ceqsexg  3609  ralab  3653  symdifass  4216  wecmpep  5624  sorpss  7683  epweon  7730  epweonALT  7731  tz7.49c  8387  dford2  9541  infxpen  9936  isacn  9966  dfac5  10051  dfackm  10089  pwfseq  10587  axgroth5  10747  axgroth6  10751  supmul  12126  elfz0lmr  13711  fsum2d  15706  cbvprod  15848  cbvprodv  15849  fprod2d  15916  rpnnen2lem12  16162  isstruct  17091  oppccatid  17654  subccatid  17782  fuccatid  17908  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  lubfun  18285  lubeldm  18286  lubelss  18287  lubval  18289  lubcl  18290  lubprop  18291  lublecl  18294  lubid  18295  glbfun  18298  glbeldm  18299  glbelss  18300  glbval  18302  glbcl  18303  glbprop  18304  joinval2  18314  joineu  18315  meetval2  18328  meeteu  18329  join0  18338  meet0  18339  odulub  18340  oduglb  18342  poslubd  18346  isglbd  18444  lubun  18450  symgsssg  19408  symgfisg  19409  pmtr3ncomlem1  19414  opprsubg  20300  lmodvscl  20841  opsrtos  22024  iscnp2  23195  cbvditg  25823  ditgsplit  25830  lgsquad2  27365  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  ltssolem1  27655  addcuts  27986  mulcut  28140  elreno2  28503  nb3grpr  29467  clwwlkccat  30077  clwlkclwwlk  30089  clwwlknccat  30150  frgr3v  30362  eqid1  30554  grpoidinv  30596  stri  32345  hstri  32353  stcltrthi  32366  sq2reunnltb  32571  nmo  32576  sgnneg  32925  elxrge02  33024  toslub  33066  tosglb  33068  xrsclat  33104  slmdvscl  33308  zarclsun  34048  unelldsys  34336  omssubadd  34478  ballotlemimin  34684  ballotlemfrcn0  34708  bnj1383  35007  bnj1386  35009  bnj153  35056  bnj543  35069  bnj544  35070  bnj546  35072  bnj605  35083  bnj579  35090  bnj600  35095  bnj601  35096  bnj852  35097  bnj893  35104  bnj906  35106  bnj917  35110  bnj938  35113  bnj944  35114  bnj998  35133  bnj1006  35136  bnj1029  35144  bnj1034  35146  bnj1124  35164  bnj1128  35166  bnj1127  35167  bnj1125  35168  bnj1147  35170  bnj1190  35184  bnj69  35186  bnj1204  35188  bnj1311  35200  bnj1318  35201  bnj1384  35208  bnj1408  35212  bnj1414  35213  bnj1415  35214  bnj1421  35218  bnj1423  35227  bnj1489  35232  bnj1493  35235  bnj60  35238  bnj1500  35244  bnj1522  35248  cvmliftlem11  35511  currybi  35904  dfon2  36006  brpprod3b  36101  brapply  36152  brrestrict  36165  dfrdg4  36167  cgr3permute3  36263  cgr3permute1  36264  cgr3permute2  36265  cgr3permute4  36266  cgr3permute5  36267  colinearxfr  36291  brsegle  36324  riotaeqi  36415  prodeq2si  36420  bj-prmoore  37368  bj-imdirco  37445  wl-equsal1t  37797  bicontr  38331  lub0N  39565  glb0N  39569  glbconN  39753  dalemeea  40039  dalem4  40041  dalem6  40044  dalem7  40045  dalem11  40050  dalem12  40051  dalem29  40077  dalem30  40078  dalem31N  40079  dalem32  40080  dalem33  40081  dalem34  40082  dalem35  40083  dalem36  40084  dalem37  40085  dalem40  40088  dalem46  40094  dalem47  40095  dalem49  40097  dalem50  40098  dalem52  40100  dalem53  40101  dalem54  40102  dalem56  40104  dalem58  40106  dalem59  40107  dalem62  40110  paddval  40174  4atexlemex4  40449  4atexlemex6  40450  cdleme31sdnN  40763  cdlemefr44  40801  cdleme48fv  40875  cdlemeg49lebilem  40915  cdleme50eq  40917  rngunsnply  43526  ifpbiidcor  43830  frege129d  44119  axfrege54a  44217  ismnuprim  44650  rr-grothprimbi  44651  iotaequ  44785  2uasban  44918  uunT1  45135  e2ebindVD  45267  e2ebindALT  45284  iunconnALT  45291  dfxlim2  46206  ioodvbdlimc1  46291  ioodvbdlimc2  46293  fourierdlem86  46550  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  hoidmvlelem1  46953  hoidmvlelem3  46955  hoidmvlelem4  46956  grtriproplem  48299  grtrif1o  48302  rngccatidALTV  48632  ringccatidALTV  48666  map0cor  49214  lubeldm2d  49317  glbeldm2d  49318  lubsscl  49319  glbsscl  49320  joindm3  49328  meetdm3  49330  isclatd  49342  ipolub00  49352  ssccatid  49431  indthinc  49821  indthincALT  49822  prsthinc  49823  mndtccatid  49946  setc1onsubc  49961