Theorem biid 251

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

Assertion

Ref	Expression
biid	|- ( ph <-> ph )

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2	1, 1	impbii 199	1 |- ( ph <-> ph )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  biidd  252  pm5.19  375  3anbi1i  1253  3anbi2i  1254  3anbi3i  1255  trubitru  1520  falbifal  1523  hadcoma  1538  hadcomb  1539  eqid  2622  abid1  2744  ceqsexg  3334  wecmpep  5106  sorpss  6942  ordon  6982  tz7.49c  7541  dford2  8517  infxpen  8837  isacn  8867  dfac5  8951  dfackm  8988  pwfseq  9486  axgroth5  9646  axgroth6  9650  supmul  10995  elfz0lmr  12583  fsum2d  14502  cbvprod  14645  fprod2d  14711  rpnnen2lem12  14954  isstruct  15870  oppccatid  16379  subccatid  16506  fuccatid  16629  setccatid  16734  catccatid  16752  estrccatid  16772  xpccatid  16828  lubfun  16980  lubeldm  16981  lubelss  16982  lubval  16984  lubcl  16985  lubprop  16986  lublecl  16989  lubid  16990  glbfun  16993  glbeldm  16994  glbelss  16995  glbval  16997  glbcl  16998  glbprop  16999  joinval2  17009  joineu  17010  meetval2  17023  meeteu  17024  isglbd  17117  lubun  17123  meet0  17137  join0  17138  oduglb  17139  odulub  17141  poslubd  17148  symgsssg  17887  symgfisg  17888  pmtr3ncomlem1  17893  opprsubg  18636  abvtriv  18841  lmodvscl  18880  opsrtos  19486  iscnp2  21043  cbvditg  23618  ditgsplit  23625  lgsquad2  25111  nb3grpr  26284  clwlkclwwlk  26903  clwlksfclwwlk  26962  frgr3v  27139  eqid1  27323  grpoidinv  27362  stri  29116  hstri  29124  stcltrthi  29137  nmo  29325  elxrge02  29640  toslub  29668  tosglb  29670  xrsclat  29680  slmdvscl  29767  unelldsys  30221  omssubadd  30362  ballotlemimin  30567  ballotlemfrcn0  30591  sgnneg  30602  bnj1383  30902  bnj1386  30904  bnj153  30950  bnj543  30963  bnj544  30964  bnj546  30966  bnj605  30977  bnj579  30984  bnj600  30989  bnj601  30990  bnj852  30991  bnj893  30998  bnj906  31000  bnj917  31004  bnj938  31007  bnj944  31008  bnj998  31026  bnj1006  31029  bnj1029  31036  bnj1034  31038  bnj1124  31056  bnj1128  31058  bnj1127  31059  bnj1125  31060  bnj1147  31062  bnj1190  31076  bnj69  31078  bnj1204  31080  bnj1311  31092  bnj1318  31093  bnj1384  31100  bnj1408  31104  bnj1414  31105  bnj1415  31106  bnj1421  31110  bnj1423  31119  bnj1489  31124  bnj1493  31127  bnj60  31130  bnj1500  31136  bnj1522  31140  cvmliftlem11  31277  dfon2  31697  sltsolem1  31826  brpprod3b  31994  brapply  32045  brrestrict  32056  dfrdg4  32058  cgr3permute3  32154  cgr3permute1  32155  cgr3permute2  32156  cgr3permute4  32157  cgr3permute5  32158  colinearxfr  32182  brsegle  32215  bj-ssbequ2  32643  bj-abid2  32782  bj-termab  32846  bj-restuni  33050  wl-equsal1t  33327  bicontr  33879  lub0N  34476  glb0N  34480  glbconN  34663  dalemeea  34949  dalem4  34951  dalem6  34954  dalem7  34955  dalem11  34960  dalem12  34961  dalem29  34987  dalem30  34988  dalem31N  34989  dalem32  34990  dalem33  34991  dalem34  34992  dalem35  34993  dalem36  34994  dalem37  34995  dalem40  34998  dalem46  35004  dalem47  35005  dalem49  35007  dalem50  35008  dalem52  35010  dalem53  35011  dalem54  35012  dalem56  35014  dalem58  35016  dalem59  35017  dalem62  35020  paddval  35084  4atexlemex4  35359  4atexlemex6  35360  cdleme31sdnN  35675  cdlemefr44  35713  cdleme48fv  35787  cdlemeg49lebilem  35827  cdleme50eq  35829  rngunsnply  37743  ifpbiidcor  37819  frege129d  38055  axfrege54a  38155  iotaequ  38630  2uasban  38778  uunT1  39007  e2ebindVD  39148  e2ebindALT  39165  iunconnALT  39172  disjinfi  39380  dfxlim2  40074  ioodvbdlimc1  40148  ioodvbdlimc2  40150  fourierdlem86  40409  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  hoidmvlelem1  40809  hoidmvlelem3  40811  hoidmvlelem4  40812  rngccatidALTV  41989  ringccatidALTV  42052