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

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

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21, 1impbii 211 1 (𝜑𝜑)
Colors of variables: wff setvar class
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  390  an21  642  3anbi1i  1153  3anbi2i  1154  3anbi3i  1155  trubitru  1562  falbifal  1565  hadcomaOLD  1596  hadcomb  1597  sb6fALT  2598  sbi2ALT  2603  sbrimALT  2605  sbanALT  2606  sbbiALT  2607  sbieALT  2609  sbiedALT  2610  sbco2ALT  2611  sb7fALT  2612  eqid  2821  abid1  2956  ceqsexg  3645  symdifass  4227  wecmpep  5541  sorpss  7448  epweon  7491  tz7.49c  8076  dford2  9077  infxpen  9434  isacn  9464  dfac5  9548  dfackm  9586  pwfseq  10080  axgroth5  10240  axgroth6  10244  supmul  11607  elfz0lmr  13146  fsum2d  15120  cbvprod  15263  fprod2d  15329  rpnnen2lem12  15572  isstruct  16490  oppccatid  16983  subccatid  17110  fuccatid  17233  setccatid  17338  catccatid  17356  estrccatid  17376  xpccatid  17432  lubfun  17584  lubeldm  17585  lubelss  17586  lubval  17588  lubcl  17589  lubprop  17590  lublecl  17593  lubid  17594  glbfun  17597  glbeldm  17598  glbelss  17599  glbval  17601  glbcl  17602  glbprop  17603  joinval2  17613  joineu  17614  meetval2  17627  meeteu  17628  isglbd  17721  lubun  17727  meet0  17741  join0  17742  oduglb  17743  odulub  17745  poslubd  17752  symgsssg  18589  symgfisg  18590  pmtr3ncomlem1  18595  opprsubg  19380  abvtriv  19606  lmodvscl  19645  opsrtos  20260  iscnp2  21841  cbvditg  24446  ditgsplit  24453  lgsquad2  25956  2sqreuop  26032  2sqreuopnn  26033  2sqreuoplt  26034  2sqreuopltb  26035  2sqreuopnnlt  26036  2sqreuopnnltb  26037  nb3grpr  27158  clwwlkccat  27762  clwlkclwwlk  27774  clwwlknccat  27836  frgr3v  28048  eqid1  28240  grpoidinv  28279  stri  30028  hstri  30036  stcltrthi  30049  sq2reunnltb  30242  nmo  30248  elxrge02  30603  toslub  30650  tosglb  30652  xrsclat  30662  slmdvscl  30837  unelldsys  31412  omssubadd  31553  ballotlemimin  31758  ballotlemfrcn0  31782  sgnneg  31793  bnj1383  32098  bnj1386  32100  bnj153  32147  bnj543  32160  bnj544  32161  bnj546  32163  bnj605  32174  bnj579  32181  bnj600  32186  bnj601  32187  bnj852  32188  bnj893  32195  bnj906  32197  bnj917  32201  bnj938  32204  bnj944  32205  bnj998  32224  bnj1006  32227  bnj1029  32235  bnj1034  32237  bnj1124  32255  bnj1128  32257  bnj1127  32258  bnj1125  32259  bnj1147  32261  bnj1190  32275  bnj69  32277  bnj1204  32279  bnj1311  32291  bnj1318  32292  bnj1384  32299  bnj1408  32303  bnj1414  32304  bnj1415  32305  bnj1421  32309  bnj1423  32318  bnj1489  32323  bnj1493  32326  bnj60  32329  bnj1500  32335  bnj1522  32339  cvmliftlem11  32537  dfon2  33032  sltsolem1  33175  brpprod3b  33343  brapply  33394  brrestrict  33405  dfrdg4  33407  cgr3permute3  33503  cgr3permute1  33504  cgr3permute2  33505  cgr3permute4  33506  cgr3permute5  33507  colinearxfr  33531  brsegle  33564  bj-prmoore  34401  wl-equsal1t  34775  bicontr  35352  lub0N  36319  glb0N  36323  glbconN  36507  dalemeea  36793  dalem4  36795  dalem6  36798  dalem7  36799  dalem11  36804  dalem12  36805  dalem29  36831  dalem30  36832  dalem31N  36833  dalem32  36834  dalem33  36835  dalem34  36836  dalem35  36837  dalem36  36838  dalem37  36839  dalem40  36842  dalem46  36848  dalem47  36849  dalem49  36851  dalem50  36852  dalem52  36854  dalem53  36855  dalem54  36856  dalem56  36858  dalem58  36860  dalem59  36861  dalem62  36864  paddval  36928  4atexlemex4  37203  4atexlemex6  37204  cdleme31sdnN  37517  cdlemefr44  37555  cdleme48fv  37629  cdlemeg49lebilem  37669  cdleme50eq  37671  rngunsnply  39766  ifpbiidcor  39833  frege129d  40101  axfrege54a  40200  ismnuprim  40623  rr-grothprimbi  40624  iotaequ  40754  2uasban  40889  uunT1  41107  e2ebindVD  41239  e2ebindALT  41256  iunconnALT  41263  disjinfi  41447  dfxlim2  42122  ioodvbdlimc1  42211  ioodvbdlimc2  42213  fourierdlem86  42471  fourierdlem94  42479  fourierdlem103  42488  fourierdlem104  42489  fourierdlem113  42498  hoidmvlelem1  42871  hoidmvlelem3  42873  hoidmvlelem4  42874  rngccatidALTV  44254  ringccatidALTV  44317
  Copyright terms: Public domain W3C validator