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 2734. (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  644  3anbi1i  1157  3anbi2i  1158  3anbi3i  1159  trubitru  1570  falbifal  1573  hadcomb  1601  eqid  2734  abid1  2870  abid2f  2927  ceqsexg  3605  ralab  3649  symdifass  4212  wecmpep  5614  sorpss  7671  epweon  7718  epweonALT  7719  tz7.49c  8375  dford2  9527  infxpen  9922  isacn  9952  dfac5  10037  dfackm  10075  pwfseq  10573  axgroth5  10733  axgroth6  10737  supmul  12112  elfz0lmr  13697  fsum2d  15692  cbvprod  15834  cbvprodv  15835  fprod2d  15902  rpnnen2lem12  16148  isstruct  17077  oppccatid  17640  subccatid  17768  fuccatid  17894  setccatid  18006  catccatid  18028  estrccatid  18053  xpccatid  18109  lubfun  18271  lubeldm  18272  lubelss  18273  lubval  18275  lubcl  18276  lubprop  18277  lublecl  18280  lubid  18281  glbfun  18284  glbeldm  18285  glbelss  18286  glbval  18288  glbcl  18289  glbprop  18290  joinval2  18300  joineu  18301  meetval2  18314  meeteu  18315  join0  18324  meet0  18325  odulub  18326  oduglb  18328  poslubd  18332  isglbd  18430  lubun  18436  symgsssg  19394  symgfisg  19395  pmtr3ncomlem1  19400  opprsubg  20286  lmodvscl  20827  opsrtos  22010  iscnp2  23181  cbvditg  25809  ditgsplit  25816  lgsquad2  27351  2sqreuop  27427  2sqreuopnn  27428  2sqreuoplt  27429  2sqreuopltb  27430  2sqreuopnnlt  27431  2sqreuopnnltb  27432  sltsolem1  27641  addscut  27948  mulscut  28101  elreno2  28440  nb3grpr  29404  clwwlkccat  30014  clwlkclwwlk  30026  clwwlknccat  30087  frgr3v  30299  eqid1  30491  grpoidinv  30532  stri  32281  hstri  32289  stcltrthi  32302  sq2reunnltb  32508  nmo  32513  sgnneg  32863  elxrge02  32962  toslub  33004  tosglb  33006  xrsclat  33042  slmdvscl  33245  zarclsun  33976  unelldsys  34264  omssubadd  34406  ballotlemimin  34612  ballotlemfrcn0  34636  bnj1383  34936  bnj1386  34938  bnj153  34985  bnj543  34998  bnj544  34999  bnj546  35001  bnj605  35012  bnj579  35019  bnj600  35024  bnj601  35025  bnj852  35026  bnj893  35033  bnj906  35035  bnj917  35039  bnj938  35042  bnj944  35043  bnj998  35062  bnj1006  35065  bnj1029  35073  bnj1034  35075  bnj1124  35093  bnj1128  35095  bnj1127  35096  bnj1125  35097  bnj1147  35099  bnj1190  35113  bnj69  35115  bnj1204  35117  bnj1311  35129  bnj1318  35130  bnj1384  35137  bnj1408  35141  bnj1414  35142  bnj1415  35143  bnj1421  35147  bnj1423  35156  bnj1489  35161  bnj1493  35164  bnj60  35167  bnj1500  35173  bnj1522  35177  cvmliftlem11  35438  currybi  35831  dfon2  35933  brpprod3b  36028  brapply  36079  brrestrict  36092  dfrdg4  36094  cgr3permute3  36190  cgr3permute1  36191  cgr3permute2  36192  cgr3permute4  36193  cgr3permute5  36194  colinearxfr  36218  brsegle  36251  riotaeqi  36342  prodeq2si  36347  bj-prmoore  37259  bj-imdirco  37334  wl-equsal1t  37686  bicontr  38220  lub0N  39388  glb0N  39392  glbconN  39576  dalemeea  39862  dalem4  39864  dalem6  39867  dalem7  39868  dalem11  39873  dalem12  39874  dalem29  39900  dalem30  39901  dalem31N  39902  dalem32  39903  dalem33  39904  dalem34  39905  dalem35  39906  dalem36  39907  dalem37  39908  dalem40  39911  dalem46  39917  dalem47  39918  dalem49  39920  dalem50  39921  dalem52  39923  dalem53  39924  dalem54  39925  dalem56  39927  dalem58  39929  dalem59  39930  dalem62  39933  paddval  39997  4atexlemex4  40272  4atexlemex6  40273  cdleme31sdnN  40586  cdlemefr44  40624  cdleme48fv  40698  cdlemeg49lebilem  40738  cdleme50eq  40740  rngunsnply  43353  ifpbiidcor  43657  frege129d  43946  axfrege54a  44044  ismnuprim  44477  rr-grothprimbi  44478  iotaequ  44612  2uasban  44745  uunT1  44962  e2ebindVD  45094  e2ebindALT  45111  iunconnALT  45118  dfxlim2  46034  ioodvbdlimc1  46119  ioodvbdlimc2  46121  fourierdlem86  46378  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem113  46405  hoidmvlelem1  46781  hoidmvlelem3  46783  hoidmvlelem4  46784  grtriproplem  48127  grtrif1o  48130  rngccatidALTV  48460  ringccatidALTV  48494  map0cor  49042  lubeldm2d  49145  glbeldm2d  49146  lubsscl  49147  glbsscl  49148  joindm3  49156  meetdm3  49158  isclatd  49170  ipolub00  49180  ssccatid  49259  indthinc  49649  indthincALT  49650  prsthinc  49651  mndtccatid  49774  setc1onsubc  49789