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 2739. (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  2739  abid1  2882  ceqsexg  3584  ralab  3629  symdifass  4186  wecmpep  5582  sorpss  7590  epweon  7634  epweonOLD  7635  tz7.49c  8286  dford2  9387  infxpen  9779  isacn  9809  dfac5  9893  dfackm  9931  pwfseq  10429  axgroth5  10589  axgroth6  10593  supmul  11956  elfz0lmr  13511  fsum2d  15492  cbvprod  15634  fprod2d  15700  rpnnen2lem12  15943  isstruct  16862  oppccatid  17439  subccatid  17570  fuccatid  17696  setccatid  17808  catccatid  17830  estrccatid  17857  xpccatid  17914  lubfun  18079  lubeldm  18080  lubelss  18081  lubval  18083  lubcl  18084  lubprop  18085  lublecl  18088  lubid  18089  glbfun  18092  glbeldm  18093  glbelss  18094  glbval  18096  glbcl  18097  glbprop  18098  joinval2  18108  joineu  18109  meetval2  18122  meeteu  18123  join0  18132  meet0  18133  odulub  18134  oduglb  18136  poslubd  18140  isglbd  18236  lubun  18242  symgsssg  19084  symgfisg  19085  pmtr3ncomlem1  19090  opprsubg  19887  abvtriv  20110  lmodvscl  20149  opsrtos  21273  iscnp2  22399  cbvditg  25027  ditgsplit  25034  lgsquad2  26543  2sqreuop  26619  2sqreuopnn  26620  2sqreuoplt  26621  2sqreuopltb  26622  2sqreuopnnlt  26623  2sqreuopnnltb  26624  nb3grpr  27758  clwwlkccat  28363  clwlkclwwlk  28375  clwwlknccat  28436  frgr3v  28648  eqid1  28840  grpoidinv  28879  stri  30628  hstri  30636  stcltrthi  30649  sq2reunnltb  30842  nmo  30847  elxrge02  31215  toslub  31260  tosglb  31262  xrsclat  31298  slmdvscl  31476  zarclsun  31829  unelldsys  32135  omssubadd  32276  ballotlemimin  32481  ballotlemfrcn0  32505  sgnneg  32516  bnj1383  32820  bnj1386  32822  bnj153  32869  bnj543  32882  bnj544  32883  bnj546  32885  bnj605  32896  bnj579  32903  bnj600  32908  bnj601  32909  bnj852  32910  bnj893  32917  bnj906  32919  bnj917  32923  bnj938  32926  bnj944  32927  bnj998  32946  bnj1006  32949  bnj1029  32957  bnj1034  32959  bnj1124  32977  bnj1128  32979  bnj1127  32980  bnj1125  32981  bnj1147  32983  bnj1190  32997  bnj69  32999  bnj1204  33001  bnj1311  33013  bnj1318  33014  bnj1384  33021  bnj1408  33025  bnj1414  33026  bnj1415  33027  bnj1421  33031  bnj1423  33040  bnj1489  33045  bnj1493  33048  bnj60  33051  bnj1500  33057  bnj1522  33061  cvmliftlem11  33266  dfon2  33777  sltsolem1  33887  brpprod3b  34198  brapply  34249  brrestrict  34260  dfrdg4  34262  cgr3permute3  34358  cgr3permute1  34359  cgr3permute2  34360  cgr3permute4  34361  cgr3permute5  34362  colinearxfr  34386  brsegle  34419  bj-prmoore  35295  bj-imdirco  35370  wl-equsal1t  35709  bicontr  36247  lub0N  37210  glb0N  37214  glbconN  37398  dalemeea  37684  dalem4  37686  dalem6  37689  dalem7  37690  dalem11  37695  dalem12  37696  dalem29  37722  dalem30  37723  dalem31N  37724  dalem32  37725  dalem33  37726  dalem34  37727  dalem35  37728  dalem36  37729  dalem37  37730  dalem40  37733  dalem46  37739  dalem47  37740  dalem49  37742  dalem50  37743  dalem52  37745  dalem53  37746  dalem54  37747  dalem56  37749  dalem58  37751  dalem59  37752  dalem62  37755  paddval  37819  4atexlemex4  38094  4atexlemex6  38095  cdleme31sdnN  38408  cdlemefr44  38446  cdleme48fv  38520  cdlemeg49lebilem  38560  cdleme50eq  38562  rngunsnply  41005  ifpbiidcor  41088  frege129d  41378  axfrege54a  41476  ismnuprim  41919  rr-grothprimbi  41920  iotaequ  42054  2uasban  42189  uunT1  42407  e2ebindVD  42539  e2ebindALT  42556  iunconnALT  42563  dfxlim2  43396  ioodvbdlimc1  43481  ioodvbdlimc2  43483  fourierdlem86  43740  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  hoidmvlelem1  44140  hoidmvlelem3  44142  hoidmvlelem4  44143  rngccatidALTV  45558  ringccatidALTV  45621  map0cor  46193  lubeldm2d  46263  glbeldm2d  46264  lubsscl  46265  glbsscl  46266  joindm3  46274  meetdm3  46276  isclatd  46280  ipolub00  46290  indthinc  46344  indthincALT  46345  prsthinc  46346  mndtccatid  46385