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

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

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21, 1impbii 210 1 (𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  biidd  263  pm5.19  388  an21  640  3anbi1i  1149  3anbi2i  1150  3anbi3i  1151  trubitru  1557  falbifal  1560  hadcomaOLD  1591  hadcomb  1592  sb6fALT  2595  sbi2ALT  2600  sbrimALT  2602  sbanALT  2603  sbbiALT  2604  sbieALT  2606  sbiedALT  2607  sbco2ALT  2608  sb7fALT  2609  eqid  2818  abid1  2953  ceqsexg  3643  symdifass  4225  wecmpep  5540  sorpss  7443  epweon  7486  tz7.49c  8071  dford2  9071  infxpen  9428  isacn  9458  dfac5  9542  dfackm  9580  pwfseq  10074  axgroth5  10234  axgroth6  10238  supmul  11601  elfz0lmr  13140  fsum2d  15114  cbvprod  15257  fprod2d  15323  rpnnen2lem12  15566  isstruct  16484  oppccatid  16977  subccatid  17104  fuccatid  17227  setccatid  17332  catccatid  17350  estrccatid  17370  xpccatid  17426  lubfun  17578  lubeldm  17579  lubelss  17580  lubval  17582  lubcl  17583  lubprop  17584  lublecl  17587  lubid  17588  glbfun  17591  glbeldm  17592  glbelss  17593  glbval  17595  glbcl  17596  glbprop  17597  joinval2  17607  joineu  17608  meetval2  17621  meeteu  17622  isglbd  17715  lubun  17721  meet0  17735  join0  17736  oduglb  17737  odulub  17739  poslubd  17746  symgsssg  18524  symgfisg  18525  pmtr3ncomlem1  18530  opprsubg  19315  abvtriv  19541  lmodvscl  19580  opsrtos  20194  iscnp2  21775  cbvditg  24379  ditgsplit  24386  lgsquad2  25889  2sqreuop  25965  2sqreuopnn  25966  2sqreuoplt  25967  2sqreuopltb  25968  2sqreuopnnlt  25969  2sqreuopnnltb  25970  nb3grpr  27091  clwwlkccat  27695  clwlkclwwlk  27707  clwwlknccat  27769  frgr3v  27981  eqid1  28173  grpoidinv  28212  stri  29961  hstri  29969  stcltrthi  29982  sq2reunnltb  30175  nmo  30181  elxrge02  30535  toslub  30582  tosglb  30584  xrsclat  30594  slmdvscl  30769  unelldsys  31316  omssubadd  31457  ballotlemimin  31662  ballotlemfrcn0  31686  sgnneg  31697  bnj1383  32002  bnj1386  32004  bnj153  32051  bnj543  32064  bnj544  32065  bnj546  32067  bnj605  32078  bnj579  32085  bnj600  32090  bnj601  32091  bnj852  32092  bnj893  32099  bnj906  32101  bnj917  32105  bnj938  32108  bnj944  32109  bnj998  32127  bnj1006  32130  bnj1029  32137  bnj1034  32139  bnj1124  32157  bnj1128  32159  bnj1127  32160  bnj1125  32161  bnj1147  32163  bnj1190  32177  bnj69  32179  bnj1204  32181  bnj1311  32193  bnj1318  32194  bnj1384  32201  bnj1408  32205  bnj1414  32206  bnj1415  32207  bnj1421  32211  bnj1423  32220  bnj1489  32225  bnj1493  32228  bnj60  32231  bnj1500  32237  bnj1522  32241  cvmliftlem11  32439  dfon2  32934  sltsolem1  33077  brpprod3b  33245  brapply  33296  brrestrict  33307  dfrdg4  33309  cgr3permute3  33405  cgr3permute1  33406  cgr3permute2  33407  cgr3permute4  33408  cgr3permute5  33409  colinearxfr  33433  brsegle  33466  wl-equsal1t  34662  bicontr  35239  lub0N  36205  glb0N  36209  glbconN  36393  dalemeea  36679  dalem4  36681  dalem6  36684  dalem7  36685  dalem11  36690  dalem12  36691  dalem29  36717  dalem30  36718  dalem31N  36719  dalem32  36720  dalem33  36721  dalem34  36722  dalem35  36723  dalem36  36724  dalem37  36725  dalem40  36728  dalem46  36734  dalem47  36735  dalem49  36737  dalem50  36738  dalem52  36740  dalem53  36741  dalem54  36742  dalem56  36744  dalem58  36746  dalem59  36747  dalem62  36750  paddval  36814  4atexlemex4  37089  4atexlemex6  37090  cdleme31sdnN  37403  cdlemefr44  37441  cdleme48fv  37515  cdlemeg49lebilem  37555  cdleme50eq  37557  rngunsnply  39651  ifpbiidcor  39718  frege129d  39986  axfrege54a  40085  ismnuprim  40507  rr-grothprimbi  40508  iotaequ  40638  2uasban  40773  uunT1  40991  e2ebindVD  41123  e2ebindALT  41140  iunconnALT  41147  disjinfi  41330  dfxlim2  42005  ioodvbdlimc1  42094  ioodvbdlimc2  42096  fourierdlem86  42354  fourierdlem94  42362  fourierdlem103  42371  fourierdlem104  42372  fourierdlem113  42381  hoidmvlelem1  42754  hoidmvlelem3  42756  hoidmvlelem4  42757  rngccatidALTV  44188  ringccatidALTV  44251
  Copyright terms: Public domain W3C validator