MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biid Structured version   Visualization version   GIF version

Theorem biid 252
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 2813. (Contributed by NM, 2-Jun-1993.)
Assertion
Ref Expression
biid (𝜑𝜑)

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21, 1impbii 200 1 (𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  biidd  253  pm5.19  376  3anbi1i  1189  3anbi2i  1190  3anbi3i  1191  trubitru  1667  falbifal  1670  hadcoma  1693  hadcomb  1694  eqid  2813  abid1  2935  ceqsexg  3535  symdifass  4058  wecmpep  5310  opelresg  5610  sorpss  7175  ordon  7215  tz7.49c  7780  dford2  8767  infxpen  9123  isacn  9153  dfac5  9237  dfackm  9276  pwfseq  9774  axgroth5  9934  axgroth6  9938  supmul  11283  elfz0lmr  12810  fsum2d  14728  cbvprod  14869  fprod2d  14935  rpnnen2lem12  15177  isstruct  16084  oppccatid  16586  subccatid  16713  fuccatid  16836  setccatid  16941  catccatid  16959  estrccatid  16979  xpccatid  17036  lubfun  17188  lubeldm  17189  lubelss  17190  lubval  17192  lubcl  17193  lubprop  17194  lublecl  17197  lubid  17198  glbfun  17201  glbeldm  17202  glbelss  17203  glbval  17205  glbcl  17206  glbprop  17207  joinval2  17217  joineu  17218  meetval2  17231  meeteu  17232  isglbd  17325  lubun  17331  meet0  17345  join0  17346  oduglb  17347  odulub  17349  poslubd  17356  symgsssg  18091  symgfisg  18092  pmtr3ncomlem1  18097  opprsubg  18841  abvtriv  19048  lmodvscl  19087  opsrtos  19697  iscnp2  21261  cbvditg  23838  ditgsplit  23845  lgsquad2  25331  nb3grpr  26506  clwwlkccat  27139  clwlkclwwlk  27151  clwwlknccat  27220  clwlksfclwwlkOLD  27242  frgr3v  27456  eqid1  27660  grpoidinv  27697  stri  29450  hstri  29458  stcltrthi  29471  nmo  29659  elxrge02  29971  toslub  29999  tosglb  30001  xrsclat  30011  slmdvscl  30098  unelldsys  30552  omssubadd  30693  ballotlemimin  30898  ballotlemfrcn0  30922  sgnneg  30933  bnj1383  31230  bnj1386  31232  bnj153  31278  bnj543  31291  bnj544  31292  bnj546  31294  bnj605  31305  bnj579  31312  bnj600  31317  bnj601  31318  bnj852  31319  bnj893  31326  bnj906  31328  bnj917  31332  bnj938  31335  bnj944  31336  bnj998  31354  bnj1006  31357  bnj1029  31364  bnj1034  31366  bnj1124  31384  bnj1128  31386  bnj1127  31387  bnj1125  31388  bnj1147  31390  bnj1190  31404  bnj69  31406  bnj1204  31408  bnj1311  31420  bnj1318  31421  bnj1384  31428  bnj1408  31432  bnj1414  31433  bnj1415  31434  bnj1421  31438  bnj1423  31447  bnj1489  31452  bnj1493  31455  bnj60  31458  bnj1500  31464  bnj1522  31468  cvmliftlem11  31605  dfon2  32022  sltsolem1  32152  brpprod3b  32320  brapply  32371  brrestrict  32382  dfrdg4  32384  cgr3permute3  32480  cgr3permute1  32481  cgr3permute2  32482  cgr3permute4  32483  cgr3permute5  32484  colinearxfr  32508  brsegle  32541  bj-ssbequ2  32963  bj-abid2  33098  bj-termab  33160  bj-restuni  33363  wl-equsal1t  33643  bicontr  34192  lub0N  34971  glb0N  34975  glbconN  35159  dalemeea  35445  dalem4  35447  dalem6  35450  dalem7  35451  dalem11  35456  dalem12  35457  dalem29  35483  dalem30  35484  dalem31N  35485  dalem32  35486  dalem33  35487  dalem34  35488  dalem35  35489  dalem36  35490  dalem37  35491  dalem40  35494  dalem46  35500  dalem47  35501  dalem49  35503  dalem50  35504  dalem52  35506  dalem53  35507  dalem54  35508  dalem56  35510  dalem58  35512  dalem59  35513  dalem62  35516  paddval  35580  4atexlemex4  35855  4atexlemex6  35856  cdleme31sdnN  36169  cdlemefr44  36207  cdleme48fv  36281  cdlemeg49lebilem  36321  cdleme50eq  36323  rngunsnply  38245  ifpbiidcor  38320  frege129d  38556  axfrege54a  38656  iotaequ  39130  2uasban  39277  uunT1  39505  e2ebindVD  39643  e2ebindALT  39660  iunconnALT  39667  disjinfi  39870  dfxlim2  40555  ioodvbdlimc1  40629  ioodvbdlimc2  40631  fourierdlem86  40889  fourierdlem94  40897  fourierdlem103  40906  fourierdlem104  40907  fourierdlem113  40916  hoidmvlelem1  41292  hoidmvlelem3  41294  hoidmvlelem4  41295  rngccatidALTV  42558  ringccatidALTV  42621
  Copyright terms: Public domain W3C validator