Theorem biid 264

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 2760. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 212	1 ⊢ (𝜑 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biidd  265  pm5.19  391  an21  657  3anbi1i  1175  3anbi2i  1176  3anbi3i  1177  trubitru  1598  falbifal  1601  hadcomb  1629  eqid  2760  abid1  2896  abid2f  2952  ceqsexg  3606  symdifass  4206  wecmpep  5643  sorpss  7748  epweon  7793  epweonALT  7794  tz7.49c  8463  dford2  9628  infxpen  10100  isacn  10130  dfac5  10214  dfackm  10252  pwfseq  10756  axgroth5  10916  axgroth6  10920  supmul  12296  elfz0lmr  13925  sgnneg  15262  fsum2d  15946  cbvprod  16091  cbvprodv  16092  fprod2d  16157  rpnnen2lem12  16402  isstruct  17339  oppccatid  17902  subccatid  18030  fuccatid  18156  setccatid  18268  catccatid  18290  estrccatid  18315  xpccatid  18371  lubfun  18533  lubeldm  18534  lubelss  18535  lubval  18537  lubcl  18538  lubprop  18539  lublecl  18542  lubid  18543  glbfun  18546  glbeldm  18547  glbelss  18548  glbval  18550  glbcl  18551  glbprop  18552  joinval2  18562  joineu  18563  meetval2  18576  meeteu  18577  join0  18586  meet0  18587  odulub  18588  oduglb  18590  poslubd  18594  isglbd  18692  lubun  18698  symgsssg  19690  symgfisg  19691  pmtr3ncomlem1  19696  opprsubg  20591  lmodvscl  21162  opsrtos  22375  iscnp2  23566  cbvditg  26183  ditgsplit  26190  lgsquad2  27722  2sqreuop  27798  2sqreuopnn  27799  2sqreuoplt  27800  2sqreuopltb  27801  2sqreuopnnlt  27802  2sqreuopnnltb  27803  ltssolem1  28041  addcuts  28373  mulcut  28527  elreno2  28890  nb3grpr  29972  clwwlkccat  30590  clwlkclwwlk  30602  clwwlknccat  30663  frgr3v  30885  eqid1  31077  grpoidinv  31119  stri  32868  hstri  32876  stcltrthi  32889  sq2reunnltb  33132  nmo  33137  elxrge02  33548  toslub  33584  tosglb  33586  xrsclat  33622  slmdvscl  33825  zarclsun  34552  unelldsys  34841  ballotlemimin  35188  ballotlemfrcn0  35212  bnj1383  35511  bnj1386  35513  bnj153  35560  bnj543  35573  bnj544  35574  bnj546  35576  bnj605  35587  bnj579  35594  bnj600  35599  bnj601  35600  bnj852  35601  bnj893  35608  bnj906  35610  bnj917  35614  bnj938  35617  bnj944  35618  bnj998  35637  bnj1006  35640  bnj1029  35648  bnj1034  35650  bnj1124  35668  bnj1128  35670  bnj1127  35671  bnj1125  35672  bnj1147  35674  bnj1190  35688  bnj69  35690  bnj1204  35692  bnj1311  35704  bnj1318  35705  bnj1384  35712  bnj1408  35716  bnj1414  35717  bnj1415  35718  bnj1421  35722  bnj1423  35731  bnj1489  35736  bnj1493  35739  bnj60  35742  bnj1500  35748  bnj1522  35752  cvmliftlem11  36150  currybi  36543  dfon2  36650  brpprod3b  36745  brapply  36796  brrestrict  36809  dfrdg4  36811  cgr3permute3  36908  cgr3permute1  36909  cgr3permute2  36910  cgr3permute4  36911  cgr3permute5  36912  colinearxfr  36936  brsegle  36969  riotaeqi  37084  prodeq2si  37089  bj-prmoore  38144  bj-imdirco  38220  wl-equsal1t  38583  bicontr  39123  lub0N  40355  glb0N  40359  glbconN  40543  dalemeea  40829  dalem4  40831  dalem6  40834  dalem7  40835  dalem11  40840  dalem12  40841  dalem29  40867  dalem30  40868  dalem31N  40869  dalem32  40870  dalem33  40871  dalem34  40872  dalem35  40873  dalem36  40874  dalem37  40875  dalem40  40878  dalem46  40884  dalem47  40885  dalem49  40887  dalem50  40888  dalem52  40890  dalem53  40891  dalem54  40892  dalem56  40894  dalem58  40896  dalem59  40897  dalem62  40900  paddval  40964  4atexlemex4  41239  4atexlemex6  41240  cdleme31sdnN  41553  cdlemefr44  41591  cdleme48fv  41665  cdlemeg49lebilem  41705  cdleme50eq  41707  rngunsnply  44280  ifpbiidcor  44584  frege129d  44872  axfrege54a  44970  ismnuprim  45387  rr-grothprimbi  45388  iotaequ  45521  2uasban  45653  uunT1  45870  e2ebindVD  46002  e2ebindALT  46019  iunconnALT  46026  dfxlim2  46966  ioodvbdlimc1  47051  ioodvbdlimc2  47053  fourierdlem86  47310  fourierdlem94  47318  fourierdlem103  47327  fourierdlem104  47328  fourierdlem113  47337  hoidmvlelem1  47713  hoidmvlelem3  47715  hoidmvlelem4  47716  grtriproplem  49145  grtrif1o  49148  rngccatidALTV  49477  ringccatidALTV  49511  map0cor  50074  lubeldm2d  50180  glbeldm2d  50181  lubsscl  50182  glbsscl  50183  joindm3  50191  meetdm3  50193  isclatd  50205  ipolub00  50215  ssccatid  50294  indthinc  50705  indthincALT  50706  prsthinc  50707  mndtccatid  50833  setc1onsubc  50848  parcatid2  50871  parcatid  50872  2alsraln0  51096