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  1156  3anbi2i  1157  3anbi3i  1158  trubitru  1565  falbifal  1568  hadcomb  1596  eqid  2734  abid1  2875  abid2f  2933  ceqsexg  3652  ralab  3699  symdifass  4267  wecmpep  5680  sorpss  7746  epweon  7793  epweonALT  7794  tz7.49c  8484  dford2  9657  infxpen  10051  isacn  10081  dfac5  10166  dfackm  10204  pwfseq  10701  axgroth5  10861  axgroth6  10865  supmul  12237  elfz0lmr  13817  fsum2d  15803  cbvprod  15945  cbvprodv  15946  fprod2d  16013  rpnnen2lem12  16257  isstruct  17185  oppccatid  17765  subccatid  17896  fuccatid  18025  setccatid  18137  catccatid  18159  estrccatid  18186  xpccatid  18243  lubfun  18409  lubeldm  18410  lubelss  18411  lubval  18413  lubcl  18414  lubprop  18415  lublecl  18418  lubid  18419  glbfun  18422  glbeldm  18423  glbelss  18424  glbval  18426  glbcl  18427  glbprop  18428  joinval2  18438  joineu  18439  meetval2  18452  meeteu  18453  join0  18462  meet0  18463  odulub  18464  oduglb  18466  poslubd  18470  isglbd  18566  lubun  18572  symgsssg  19499  symgfisg  19500  pmtr3ncomlem1  19505  opprsubg  20368  lmodvscl  20892  opsrtos  22098  iscnp2  23262  cbvditg  25903  ditgsplit  25910  lgsquad2  27444  2sqreuop  27520  2sqreuopnn  27521  2sqreuoplt  27522  2sqreuopltb  27523  2sqreuopnnlt  27524  2sqreuopnnltb  27525  sltsolem1  27734  addscut  28025  mulscut  28172  nb3grpr  29413  clwwlkccat  30018  clwlkclwwlk  30030  clwwlknccat  30091  frgr3v  30303  eqid1  30495  grpoidinv  30536  stri  32285  hstri  32293  stcltrthi  32306  sq2reunnltb  32512  nmo  32517  elxrge02  32898  toslub  32947  tosglb  32949  xrsclat  32995  slmdvscl  33202  zarclsun  33830  unelldsys  34138  omssubadd  34281  ballotlemimin  34486  ballotlemfrcn0  34510  sgnneg  34521  bnj1383  34823  bnj1386  34825  bnj153  34872  bnj543  34885  bnj544  34886  bnj546  34888  bnj605  34899  bnj579  34906  bnj600  34911  bnj601  34912  bnj852  34913  bnj893  34920  bnj906  34922  bnj917  34926  bnj938  34929  bnj944  34930  bnj998  34949  bnj1006  34952  bnj1029  34960  bnj1034  34962  bnj1124  34980  bnj1128  34982  bnj1127  34983  bnj1125  34984  bnj1147  34986  bnj1190  35000  bnj69  35002  bnj1204  35004  bnj1311  35016  bnj1318  35017  bnj1384  35024  bnj1408  35028  bnj1414  35029  bnj1415  35030  bnj1421  35034  bnj1423  35043  bnj1489  35048  bnj1493  35051  bnj60  35054  bnj1500  35060  bnj1522  35064  cvmliftlem11  35279  currybi  35672  dfon2  35773  brpprod3b  35868  brapply  35919  brrestrict  35930  dfrdg4  35932  cgr3permute3  36028  cgr3permute1  36029  cgr3permute2  36030  cgr3permute4  36031  cgr3permute5  36032  colinearxfr  36056  brsegle  36089  riotaeqi  36180  prodeq2si  36185  bj-prmoore  37097  bj-imdirco  37172  wl-equsal1t  37522  bicontr  38066  lub0N  39170  glb0N  39174  glbconN  39358  glbconNOLD  39359  dalemeea  39645  dalem4  39647  dalem6  39650  dalem7  39651  dalem11  39656  dalem12  39657  dalem29  39683  dalem30  39684  dalem31N  39685  dalem32  39686  dalem33  39687  dalem34  39688  dalem35  39689  dalem36  39690  dalem37  39691  dalem40  39694  dalem46  39700  dalem47  39701  dalem49  39703  dalem50  39704  dalem52  39706  dalem53  39707  dalem54  39708  dalem56  39710  dalem58  39712  dalem59  39713  dalem62  39716  paddval  39780  4atexlemex4  40055  4atexlemex6  40056  cdleme31sdnN  40369  cdlemefr44  40407  cdleme48fv  40481  cdlemeg49lebilem  40521  cdleme50eq  40523  rngunsnply  43157  ifpbiidcor  43463  frege129d  43752  axfrege54a  43850  ismnuprim  44289  rr-grothprimbi  44290  iotaequ  44424  2uasban  44559  uunT1  44777  e2ebindVD  44909  e2ebindALT  44926  iunconnALT  44933  dfxlim2  45803  ioodvbdlimc1  45888  ioodvbdlimc2  45890  fourierdlem86  46147  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  hoidmvlelem1  46550  hoidmvlelem3  46552  hoidmvlelem4  46553  grtriproplem  47843  grtrif1o  47846  rngccatidALTV  48115  ringccatidALTV  48149  map0cor  48684  lubeldm2d  48754  glbeldm2d  48755  lubsscl  48756  glbsscl  48757  joindm3  48765  meetdm3  48767  isclatd  48771  ipolub00  48781  indthinc  48852  indthincALT  48853  prsthinc  48854  mndtccatid  48895