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 2651. (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  374  3anbi1i  1272  3anbi2i  1273  3anbi3i  1274  trubitru  1560  falbifal  1563  hadcoma  1578  hadcomb  1579  eqid  2651  abid1  2773  ceqsexg  3365  wecmpep  5135  opelresg  5434  sorpss  6984  ordon  7024  tz7.49c  7586  dford2  8555  infxpen  8875  isacn  8905  dfac5  8989  dfackm  9026  pwfseq  9524  axgroth5  9684  axgroth6  9688  supmul  11033  elfz0lmr  12623  fsum2d  14546  cbvprod  14689  fprod2d  14755  rpnnen2lem12  14998  isstruct  15917  oppccatid  16426  subccatid  16553  fuccatid  16676  setccatid  16781  catccatid  16799  estrccatid  16819  xpccatid  16875  lubfun  17027  lubeldm  17028  lubelss  17029  lubval  17031  lubcl  17032  lubprop  17033  lublecl  17036  lubid  17037  glbfun  17040  glbeldm  17041  glbelss  17042  glbval  17044  glbcl  17045  glbprop  17046  joinval2  17056  joineu  17057  meetval2  17070  meeteu  17071  isglbd  17164  lubun  17170  meet0  17184  join0  17185  oduglb  17186  odulub  17188  poslubd  17195  symgsssg  17933  symgfisg  17934  pmtr3ncomlem1  17939  opprsubg  18682  abvtriv  18889  lmodvscl  18928  opsrtos  19534  iscnp2  21091  cbvditg  23663  ditgsplit  23670  lgsquad2  25156  nb3grpr  26328  clwlkclwwlk  26968  clwlksfclwwlk  27049  frgr3v  27255  clwwlkccat  27332  clwwlknccat  27333  eqid1  27453  grpoidinv  27490  stri  29244  hstri  29252  stcltrthi  29265  nmo  29453  elxrge02  29768  toslub  29796  tosglb  29798  xrsclat  29808  slmdvscl  29895  unelldsys  30349  omssubadd  30490  ballotlemimin  30695  ballotlemfrcn0  30719  sgnneg  30730  bnj1383  31028  bnj1386  31030  bnj153  31076  bnj543  31089  bnj544  31090  bnj546  31092  bnj605  31103  bnj579  31110  bnj600  31115  bnj601  31116  bnj852  31117  bnj893  31124  bnj906  31126  bnj917  31130  bnj938  31133  bnj944  31134  bnj998  31152  bnj1006  31155  bnj1029  31162  bnj1034  31164  bnj1124  31182  bnj1128  31184  bnj1127  31185  bnj1125  31186  bnj1147  31188  bnj1190  31202  bnj69  31204  bnj1204  31206  bnj1311  31218  bnj1318  31219  bnj1384  31226  bnj1408  31230  bnj1414  31231  bnj1415  31232  bnj1421  31236  bnj1423  31245  bnj1489  31250  bnj1493  31253  bnj60  31256  bnj1500  31262  bnj1522  31266  cvmliftlem11  31403  dfon2  31821  sltsolem1  31951  brpprod3b  32119  brapply  32170  brrestrict  32181  dfrdg4  32183  cgr3permute3  32279  cgr3permute1  32280  cgr3permute2  32281  cgr3permute4  32282  cgr3permute5  32283  colinearxfr  32307  brsegle  32340  bj-ssbequ2  32768  bj-abid2  32907  bj-termab  32971  bj-restuni  33175  wl-equsal1t  33457  bicontr  34009  lub0N  34794  glb0N  34798  glbconN  34981  dalemeea  35267  dalem4  35269  dalem6  35272  dalem7  35273  dalem11  35278  dalem12  35279  dalem29  35305  dalem30  35306  dalem31N  35307  dalem32  35308  dalem33  35309  dalem34  35310  dalem35  35311  dalem36  35312  dalem37  35313  dalem40  35316  dalem46  35322  dalem47  35323  dalem49  35325  dalem50  35326  dalem52  35328  dalem53  35329  dalem54  35330  dalem56  35332  dalem58  35334  dalem59  35335  dalem62  35338  paddval  35402  4atexlemex4  35677  4atexlemex6  35678  cdleme31sdnN  35992  cdlemefr44  36030  cdleme48fv  36104  cdlemeg49lebilem  36144  cdleme50eq  36146  rngunsnply  38060  ifpbiidcor  38136  frege129d  38372  axfrege54a  38472  iotaequ  38947  2uasban  39095  uunT1  39324  e2ebindVD  39462  e2ebindALT  39479  iunconnALT  39486  disjinfi  39694  dfxlim2  40392  ioodvbdlimc1  40466  ioodvbdlimc2  40468  fourierdlem86  40727  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  hoidmvlelem1  41130  hoidmvlelem3  41132  hoidmvlelem4  41133  rngccatidALTV  42314  ringccatidALTV  42377
  Copyright terms: Public domain W3C validator