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 2733. (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  262  pm5.19  388  an21  643  3anbi1i  1158  3anbi2i  1159  3anbi3i  1160  trubitru  1571  falbifal  1574  hadcomb  1602  eqid  2733  abid1  2871  abid2f  2937  ceqsexg  3642  ralab  3688  symdifass  4252  wecmpep  5669  sorpss  7718  epweon  7762  epweonALT  7763  tz7.49c  8446  dford2  9615  infxpen  10009  isacn  10039  dfac5  10123  dfackm  10161  pwfseq  10659  axgroth5  10819  axgroth6  10823  supmul  12186  elfz0lmr  13747  fsum2d  15717  cbvprod  15859  fprod2d  15925  rpnnen2lem12  16168  isstruct  17085  oppccatid  17665  subccatid  17796  fuccatid  17922  setccatid  18034  catccatid  18056  estrccatid  18083  xpccatid  18140  lubfun  18305  lubeldm  18306  lubelss  18307  lubval  18309  lubcl  18310  lubprop  18311  lublecl  18314  lubid  18315  glbfun  18318  glbeldm  18319  glbelss  18320  glbval  18322  glbcl  18323  glbprop  18324  joinval2  18334  joineu  18335  meetval2  18348  meeteu  18349  join0  18358  meet0  18359  odulub  18360  oduglb  18362  poslubd  18366  isglbd  18462  lubun  18468  symgsssg  19335  symgfisg  19336  pmtr3ncomlem1  19341  opprsubg  20166  abvtriv  20449  lmodvscl  20489  opsrtos  21618  iscnp2  22743  cbvditg  25371  ditgsplit  25378  lgsquad2  26889  2sqreuop  26965  2sqreuopnn  26966  2sqreuoplt  26967  2sqreuopltb  26968  2sqreuopnnlt  26969  2sqreuopnnltb  26970  sltsolem1  27178  addscut  27462  mulscut  27588  nb3grpr  28639  clwwlkccat  29243  clwlkclwwlk  29255  clwwlknccat  29316  frgr3v  29528  eqid1  29720  grpoidinv  29761  stri  31510  hstri  31518  stcltrthi  31531  sq2reunnltb  31725  nmo  31730  elxrge02  32098  toslub  32143  tosglb  32145  xrsclat  32181  slmdvscl  32359  zarclsun  32850  unelldsys  33156  omssubadd  33299  ballotlemimin  33504  ballotlemfrcn0  33528  sgnneg  33539  bnj1383  33842  bnj1386  33844  bnj153  33891  bnj543  33904  bnj544  33905  bnj546  33907  bnj605  33918  bnj579  33925  bnj600  33930  bnj601  33931  bnj852  33932  bnj893  33939  bnj906  33941  bnj917  33945  bnj938  33948  bnj944  33949  bnj998  33968  bnj1006  33971  bnj1029  33979  bnj1034  33981  bnj1124  33999  bnj1128  34001  bnj1127  34002  bnj1125  34003  bnj1147  34005  bnj1190  34019  bnj69  34021  bnj1204  34023  bnj1311  34035  bnj1318  34036  bnj1384  34043  bnj1408  34047  bnj1414  34048  bnj1415  34049  bnj1421  34053  bnj1423  34062  bnj1489  34067  bnj1493  34070  bnj60  34073  bnj1500  34079  bnj1522  34083  cvmliftlem11  34286  currybi  34669  dfon2  34764  brpprod3b  34859  brapply  34910  brrestrict  34921  dfrdg4  34923  cgr3permute3  35019  cgr3permute1  35020  cgr3permute2  35021  cgr3permute4  35022  cgr3permute5  35023  colinearxfr  35047  brsegle  35080  bj-prmoore  35996  bj-imdirco  36071  wl-equsal1t  36410  bicontr  36948  lub0N  38059  glb0N  38063  glbconN  38247  glbconNOLD  38248  dalemeea  38534  dalem4  38536  dalem6  38539  dalem7  38540  dalem11  38545  dalem12  38546  dalem29  38572  dalem30  38573  dalem31N  38574  dalem32  38575  dalem33  38576  dalem34  38577  dalem35  38578  dalem36  38579  dalem37  38580  dalem40  38583  dalem46  38589  dalem47  38590  dalem49  38592  dalem50  38593  dalem52  38595  dalem53  38596  dalem54  38597  dalem56  38599  dalem58  38601  dalem59  38602  dalem62  38605  paddval  38669  4atexlemex4  38944  4atexlemex6  38945  cdleme31sdnN  39258  cdlemefr44  39296  cdleme48fv  39370  cdlemeg49lebilem  39410  cdleme50eq  39412  rngunsnply  41915  ifpbiidcor  42225  frege129d  42514  axfrege54a  42612  ismnuprim  43053  rr-grothprimbi  43054  iotaequ  43188  2uasban  43323  uunT1  43541  e2ebindVD  43673  e2ebindALT  43690  iunconnALT  43697  dfxlim2  44564  ioodvbdlimc1  44649  ioodvbdlimc2  44651  fourierdlem86  44908  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  hoidmvlelem1  45311  hoidmvlelem3  45313  hoidmvlelem4  45314  rngccatidALTV  46887  ringccatidALTV  46950  map0cor  47521  lubeldm2d  47591  glbeldm2d  47592  lubsscl  47593  glbsscl  47594  joindm3  47602  meetdm3  47604  isclatd  47608  ipolub00  47618  indthinc  47672  indthincALT  47673  prsthinc  47674  mndtccatid  47713