Theorem biid 263

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 2762. (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 211	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  biidd  264  pm5.19  389  an21  654  3anbi1i  1170  3anbi2i  1171  3anbi3i  1172  trubitru  1589  falbifal  1592  hadcomb  1620  eqid  2762  abid1  2898  abid2f  2954  ceqsexg  3612  symdifass  4214  wecmpep  5639  sorpss  7711  epweon  7758  epweonALT  7759  tz7.49c  8417  dford2  9575  infxpen  9970  isacn  10000  dfac5  10085  dfackm  10123  pwfseq  10622  axgroth5  10782  axgroth6  10786  supmul  12164  elfz0lmr  13789  sgnneg  15113  fsum2d  15798  cbvprod  15943  cbvprodv  15944  fprod2d  16011  rpnnen2lem12  16257  isstruct  17188  oppccatid  17751  subccatid  17879  fuccatid  18005  setccatid  18117  catccatid  18139  estrccatid  18164  xpccatid  18220  lubfun  18382  lubeldm  18383  lubelss  18384  lubval  18386  lubcl  18387  lubprop  18388  lublecl  18391  lubid  18392  glbfun  18395  glbeldm  18396  glbelss  18397  glbval  18399  glbcl  18400  glbprop  18401  joinval2  18411  joineu  18412  meetval2  18425  meeteu  18426  join0  18435  meet0  18436  odulub  18437  oduglb  18439  poslubd  18443  isglbd  18541  lubun  18547  symgsssg  19507  symgfisg  19508  pmtr3ncomlem1  19513  opprsubg  20397  lmodvscl  20942  opsrtos  22107  iscnp2  23296  cbvditg  25913  ditgsplit  25920  lgsquad2  27447  2sqreuop  27523  2sqreuopnn  27524  2sqreuoplt  27525  2sqreuopltb  27526  2sqreuopnnlt  27527  2sqreuopnnltb  27528  ltssolem1  27736  addcuts  28068  mulcut  28222  elreno2  28585  nb3grpr  29580  clwwlkccat  30189  clwlkclwwlk  30201  clwwlknccat  30262  frgr3v  30474  eqid1  30666  grpoidinv  30708  stri  32457  hstri  32465  stcltrthi  32478  sq2reunnltb  32681  nmo  32686  elxrge02  33106  toslub  33148  tosglb  33150  xrsclat  33186  slmdvscl  33391  zarclsun  34164  unelldsys  34452  omssubadd  34594  ballotlemimin  34800  ballotlemfrcn0  34824  bnj1383  35123  bnj1386  35125  bnj153  35172  bnj543  35185  bnj544  35186  bnj546  35188  bnj605  35199  bnj579  35206  bnj600  35211  bnj601  35212  bnj852  35213  bnj893  35220  bnj906  35222  bnj917  35226  bnj938  35229  bnj944  35230  bnj998  35249  bnj1006  35252  bnj1029  35260  bnj1034  35262  bnj1124  35280  bnj1128  35282  bnj1127  35283  bnj1125  35284  bnj1147  35286  bnj1190  35300  bnj69  35302  bnj1204  35304  bnj1311  35316  bnj1318  35317  bnj1384  35324  bnj1408  35328  bnj1414  35329  bnj1415  35330  bnj1421  35334  bnj1423  35343  bnj1489  35348  bnj1493  35351  bnj60  35354  bnj1500  35360  bnj1522  35364  cvmliftlem11  35642  currybi  36035  dfon2  36137  brpprod3b  36232  brapply  36283  brrestrict  36296  dfrdg4  36298  cgr3permute3  36394  cgr3permute1  36395  cgr3permute2  36396  cgr3permute4  36397  cgr3permute5  36398  colinearxfr  36422  brsegle  36455  riotaeqi  36556  prodeq2si  36561  bj-prmoore  37602  bj-imdirco  37679  wl-equsal1t  38042  bicontr  38576  lub0N  39810  glb0N  39814  glbconN  39998  dalemeea  40284  dalem4  40286  dalem6  40289  dalem7  40290  dalem11  40295  dalem12  40296  dalem29  40322  dalem30  40323  dalem31N  40324  dalem32  40325  dalem33  40326  dalem34  40327  dalem35  40328  dalem36  40329  dalem37  40330  dalem40  40333  dalem46  40339  dalem47  40340  dalem49  40342  dalem50  40343  dalem52  40345  dalem53  40346  dalem54  40347  dalem56  40349  dalem58  40351  dalem59  40352  dalem62  40355  paddval  40419  4atexlemex4  40694  4atexlemex6  40695  cdleme31sdnN  41008  cdlemefr44  41046  cdleme48fv  41120  cdlemeg49lebilem  41160  cdleme50eq  41162  rngunsnply  43743  ifpbiidcor  44047  frege129d  44336  axfrege54a  44434  ismnuprim  44867  rr-grothprimbi  44868  iotaequ  45002  2uasban  45135  uunT1  45352  e2ebindVD  45484  e2ebindALT  45501  iunconnALT  45508  dfxlim2  46419  ioodvbdlimc1  46504  ioodvbdlimc2  46506  fourierdlem86  46763  fourierdlem94  46771  fourierdlem103  46780  fourierdlem104  46781  fourierdlem113  46790  hoidmvlelem1  47166  hoidmvlelem3  47168  hoidmvlelem4  47169  grtriproplem  48558  grtrif1o  48561  rngccatidALTV  48891  ringccatidALTV  48925  map0cor  49473  lubeldm2d  49576  glbeldm2d  49577  lubsscl  49578  glbsscl  49579  joindm3  49587  meetdm3  49589  isclatd  49601  ipolub00  49611  ssccatid  49690  indthinc  50080  indthincALT  50081  prsthinc  50082  mndtccatid  50205  setc1onsubc  50220