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 2729. (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  1569  falbifal  1572  hadcomb  1600  eqid  2729  abid1  2864  abid2f  2922  ceqsexg  3619  ralab  3664  symdifass  4225  wecmpep  5630  sorpss  7704  epweon  7751  epweonALT  7752  tz7.49c  8414  dford2  9573  infxpen  9967  isacn  9997  dfac5  10082  dfackm  10120  pwfseq  10617  axgroth5  10777  axgroth6  10781  supmul  12155  elfz0lmr  13743  fsum2d  15737  cbvprod  15879  cbvprodv  15880  fprod2d  15947  rpnnen2lem12  16193  isstruct  17122  oppccatid  17680  subccatid  17808  fuccatid  17934  setccatid  18046  catccatid  18068  estrccatid  18093  xpccatid  18149  lubfun  18311  lubeldm  18312  lubelss  18313  lubval  18315  lubcl  18316  lubprop  18317  lublecl  18320  lubid  18321  glbfun  18324  glbeldm  18325  glbelss  18326  glbval  18328  glbcl  18329  glbprop  18330  joinval2  18340  joineu  18341  meetval2  18354  meeteu  18355  join0  18364  meet0  18365  odulub  18366  oduglb  18368  poslubd  18372  isglbd  18468  lubun  18474  symgsssg  19397  symgfisg  19398  pmtr3ncomlem1  19403  opprsubg  20261  lmodvscl  20784  opsrtos  21964  iscnp2  23126  cbvditg  25755  ditgsplit  25762  lgsquad2  27297  2sqreuop  27373  2sqreuopnn  27374  2sqreuoplt  27375  2sqreuopltb  27376  2sqreuopnnlt  27377  2sqreuopnnltb  27378  sltsolem1  27587  addscut  27885  mulscut  28035  nb3grpr  29309  clwwlkccat  29919  clwlkclwwlk  29931  clwwlknccat  29992  frgr3v  30204  eqid1  30396  grpoidinv  30437  stri  32186  hstri  32194  stcltrthi  32207  sq2reunnltb  32414  nmo  32419  sgnneg  32758  elxrge02  32852  toslub  32899  tosglb  32901  xrsclat  32949  slmdvscl  33167  zarclsun  33860  unelldsys  34148  omssubadd  34291  ballotlemimin  34497  ballotlemfrcn0  34521  bnj1383  34821  bnj1386  34823  bnj153  34870  bnj543  34883  bnj544  34884  bnj546  34886  bnj605  34897  bnj579  34904  bnj600  34909  bnj601  34910  bnj852  34911  bnj893  34918  bnj906  34920  bnj917  34924  bnj938  34927  bnj944  34928  bnj998  34947  bnj1006  34950  bnj1029  34958  bnj1034  34960  bnj1124  34978  bnj1128  34980  bnj1127  34981  bnj1125  34982  bnj1147  34984  bnj1190  34998  bnj69  35000  bnj1204  35002  bnj1311  35014  bnj1318  35015  bnj1384  35022  bnj1408  35026  bnj1414  35027  bnj1415  35028  bnj1421  35032  bnj1423  35041  bnj1489  35046  bnj1493  35049  bnj60  35052  bnj1500  35058  bnj1522  35062  cvmliftlem11  35282  currybi  35675  dfon2  35780  brpprod3b  35875  brapply  35926  brrestrict  35937  dfrdg4  35939  cgr3permute3  36035  cgr3permute1  36036  cgr3permute2  36037  cgr3permute4  36038  cgr3permute5  36039  colinearxfr  36063  brsegle  36096  riotaeqi  36187  prodeq2si  36192  bj-prmoore  37103  bj-imdirco  37178  wl-equsal1t  37530  bicontr  38074  lub0N  39182  glb0N  39186  glbconN  39370  glbconNOLD  39371  dalemeea  39657  dalem4  39659  dalem6  39662  dalem7  39663  dalem11  39668  dalem12  39669  dalem29  39695  dalem30  39696  dalem31N  39697  dalem32  39698  dalem33  39699  dalem34  39700  dalem35  39701  dalem36  39702  dalem37  39703  dalem40  39706  dalem46  39712  dalem47  39713  dalem49  39715  dalem50  39716  dalem52  39718  dalem53  39719  dalem54  39720  dalem56  39722  dalem58  39724  dalem59  39725  dalem62  39728  paddval  39792  4atexlemex4  40067  4atexlemex6  40068  cdleme31sdnN  40381  cdlemefr44  40419  cdleme48fv  40493  cdlemeg49lebilem  40533  cdleme50eq  40535  rngunsnply  43158  ifpbiidcor  43463  frege129d  43752  axfrege54a  43850  ismnuprim  44283  rr-grothprimbi  44284  iotaequ  44418  2uasban  44552  uunT1  44769  e2ebindVD  44901  e2ebindALT  44918  iunconnALT  44925  dfxlim2  45846  ioodvbdlimc1  45931  ioodvbdlimc2  45933  fourierdlem86  46190  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  hoidmvlelem1  46593  hoidmvlelem3  46595  hoidmvlelem4  46596  grtriproplem  47938  grtrif1o  47941  rngccatidALTV  48260  ringccatidALTV  48294  map0cor  48843  lubeldm2d  48946  glbeldm2d  48947  lubsscl  48948  glbsscl  48949  joindm3  48957  meetdm3  48959  isclatd  48971  ipolub00  48981  ssccatid  49061  indthinc  49451  indthincALT  49452  prsthinc  49453  mndtccatid  49576  setc1onsubc  49591