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

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

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21, 1impbii 199 1 (𝜑𝜑)
Colors of variables: wff setvar class
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  1251  3anbi2i  1252  3anbi3i  1253  trubitru  1518  falbifal  1521  hadcoma  1536  hadcomb  1537  eqid  2620  abid1  2742  ceqsexg  3328  wecmpep  5096  sorpss  6927  ordon  6967  tz7.49c  7526  dford2  8502  infxpen  8822  isacn  8852  dfac5  8936  dfackm  8973  pwfseq  9471  axgroth5  9631  axgroth6  9635  supmul  10980  elfz0lmr  12566  fsum2d  14483  cbvprod  14626  fprod2d  14692  rpnnen2lem12  14935  isstruct  15851  oppccatid  16360  subccatid  16487  fuccatid  16610  setccatid  16715  catccatid  16733  estrccatid  16753  xpccatid  16809  lubfun  16961  lubeldm  16962  lubelss  16963  lubval  16965  lubcl  16966  lubprop  16967  lublecl  16970  lubid  16971  glbfun  16974  glbeldm  16975  glbelss  16976  glbval  16978  glbcl  16979  glbprop  16980  joinval2  16990  joineu  16991  meetval2  17004  meeteu  17005  isglbd  17098  lubun  17104  meet0  17118  join0  17119  oduglb  17120  odulub  17122  poslubd  17129  symgsssg  17868  symgfisg  17869  pmtr3ncomlem1  17874  opprsubg  18617  abvtriv  18822  lmodvscl  18861  opsrtos  19467  iscnp2  21024  cbvditg  23599  ditgsplit  23606  lgsquad2  25092  nb3grpr  26265  clwlkclwwlk  26884  clwlksfclwwlk  26942  frgr3v  27119  eqid1  27293  grpoidinv  27332  stri  29086  hstri  29094  stcltrthi  29107  nmo  29297  elxrge02  29614  toslub  29642  tosglb  29644  xrsclat  29654  slmdvscl  29741  unelldsys  30195  omssubadd  30336  ballotlemimin  30541  ballotlemfrcn0  30565  sgnneg  30576  bnj1383  30876  bnj1386  30878  bnj153  30924  bnj543  30937  bnj544  30938  bnj546  30940  bnj605  30951  bnj579  30958  bnj600  30963  bnj601  30964  bnj852  30965  bnj893  30972  bnj906  30974  bnj917  30978  bnj938  30981  bnj944  30982  bnj998  31000  bnj1006  31003  bnj1029  31010  bnj1034  31012  bnj1124  31030  bnj1128  31032  bnj1127  31033  bnj1125  31034  bnj1147  31036  bnj1190  31050  bnj69  31052  bnj1204  31054  bnj1311  31066  bnj1318  31067  bnj1384  31074  bnj1408  31078  bnj1414  31079  bnj1415  31080  bnj1421  31084  bnj1423  31093  bnj1489  31098  bnj1493  31101  bnj60  31104  bnj1500  31110  bnj1522  31114  cvmliftlem11  31251  dfon2  31671  sltsolem1  31800  brpprod3b  31969  brapply  32020  brrestrict  32031  dfrdg4  32033  cgr3permute3  32129  cgr3permute1  32130  cgr3permute2  32131  cgr3permute4  32132  cgr3permute5  32133  colinearxfr  32157  brsegle  32190  bj-ssbequ2  32618  bj-abid2  32757  bj-termab  32821  bj-restuni  33025  wl-equsal1t  33298  bicontr  33850  lub0N  34295  glb0N  34299  glbconN  34482  dalemeea  34768  dalem4  34770  dalem6  34773  dalem7  34774  dalem11  34779  dalem12  34780  dalem29  34806  dalem30  34807  dalem31N  34808  dalem32  34809  dalem33  34810  dalem34  34811  dalem35  34812  dalem36  34813  dalem37  34814  dalem40  34817  dalem46  34823  dalem47  34824  dalem49  34826  dalem50  34827  dalem52  34829  dalem53  34830  dalem54  34831  dalem56  34833  dalem58  34835  dalem59  34836  dalem62  34839  paddval  34903  4atexlemex4  35178  4atexlemex6  35179  cdleme31sdnN  35494  cdlemefr44  35532  cdleme48fv  35606  cdlemeg49lebilem  35646  cdleme50eq  35648  rngunsnply  37562  ifpbiidcor  37638  frege129d  37874  axfrege54a  37975  iotaequ  38450  2uasban  38598  uunT1  38827  e2ebindVD  38968  e2ebindALT  38985  iunconnALT  38992  disjinfi  39196  ioodvbdlimc1  39911  ioodvbdlimc2  39913  fourierdlem86  40172  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem113  40199  hoidmvlelem1  40572  hoidmvlelem3  40574  hoidmvlelem4  40575  rngccatidALTV  41754  ringccatidALTV  41817
  Copyright terms: Public domain W3C validator