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

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

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21, 1impbii 197 1 (𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  biidd  250  pm5.19  373  3anbi1i  1245  3anbi2i  1246  3anbi3i  1247  trubitru  1510  falbifal  1513  hadcoma  1528  hadcomb  1529  eqid  2606  abid1  2727  ceqsexg  3300  wecmpep  5017  sorpss  6814  ordon  6848  tz7.49c  7402  dford2  8374  infxpen  8694  isacn  8724  dfac5  8808  dfackm  8845  pwfseq  9339  axgroth5  9499  axgroth6  9503  supmul  10839  fsum2d  14287  cbvprod  14427  fprod2d  14493  rpnnen2lem12  14736  isstruct  15648  oppccatid  16145  subccatid  16272  fuccatid  16395  setccatid  16500  catccatid  16518  estrccatid  16538  xpccatid  16594  lubfun  16746  lubeldm  16747  lubelss  16748  lubval  16750  lubcl  16751  lubprop  16752  lublecl  16755  lubid  16756  glbfun  16759  glbeldm  16760  glbelss  16761  glbval  16763  glbcl  16764  glbprop  16765  joinval2  16775  joineu  16776  meetval2  16789  meeteu  16790  isglbd  16883  lubun  16889  meet0  16903  join0  16904  oduglb  16905  odulub  16907  poslubd  16914  symgsssg  17653  symgfisg  17654  pmtr3ncomlem1  17659  opprsubg  18402  abvtriv  18607  lmodvscl  18646  opsrtos  19250  iscnp2  20792  cbvditg  23338  ditgsplit  23345  lgsquad2  24825  nb3grapr  25745  frgra3v  26292  eqid1  26478  grpoidinv  26509  stri  28303  hstri  28311  stcltrthi  28324  nmo  28512  elxrge02  28774  toslub  28802  tosglb  28804  xrsclat  28814  slmdvscl  28901  unelldsys  29351  omssubadd  29492  ballotlemimin  29697  ballotlemfrcn0  29721  sgnneg  29732  bnj1383  29959  bnj1386  29961  bnj153  30007  bnj543  30020  bnj544  30021  bnj546  30023  bnj605  30034  bnj579  30041  bnj600  30046  bnj601  30047  bnj852  30048  bnj893  30055  bnj906  30057  bnj917  30061  bnj938  30064  bnj944  30065  bnj998  30083  bnj1006  30086  bnj1029  30093  bnj1034  30095  bnj1124  30113  bnj1128  30115  bnj1127  30116  bnj1125  30117  bnj1147  30119  bnj1190  30133  bnj69  30135  bnj1204  30137  bnj1311  30149  bnj1318  30150  bnj1384  30157  bnj1408  30161  bnj1414  30162  bnj1415  30163  bnj1421  30167  bnj1423  30176  bnj1489  30181  bnj1493  30184  bnj60  30187  bnj1500  30193  bnj1522  30197  cvmliftlem11  30334  socnv  30711  dfon2  30744  sltsolem1  30870  brpprod3b  30967  brapply  31018  brrestrict  31029  dfrdg4  31031  cgr3permute3  31127  cgr3permute1  31128  cgr3permute2  31129  cgr3permute4  31130  cgr3permute5  31131  colinearxfr  31155  brsegle  31188  bj-ssbequ2  31635  bj-abid2  31780  bj-termab  31839  bj-restuni  32031  wl-equsal1t  32306  bicontr  32849  elimhyps  33065  lub0N  33294  glb0N  33298  glbconN  33481  dalemeea  33767  dalem4  33769  dalem6  33772  dalem7  33773  dalem11  33778  dalem12  33779  dalem29  33805  dalem30  33806  dalem31N  33807  dalem32  33808  dalem33  33809  dalem34  33810  dalem35  33811  dalem36  33812  dalem37  33813  dalem40  33816  dalem46  33822  dalem47  33823  dalem49  33825  dalem50  33826  dalem52  33828  dalem53  33829  dalem54  33830  dalem56  33832  dalem58  33834  dalem59  33835  dalem62  33838  paddval  33902  4atexlemex4  34177  4atexlemex6  34178  cdleme31sdnN  34493  cdlemefr44  34531  cdleme48fv  34605  cdlemeg49lebilem  34645  cdleme50eq  34647  rngunsnply  36562  ifpbiidcor  36638  frege129d  36874  axfrege54a  36975  iotaequ  37452  2uasban  37599  uunT1  37828  e2ebindVD  37970  e2ebindALT  37987  iunconALT  37994  disjinfi  38175  ioodvbdlimc1  38624  ioodvbdlimc2  38626  fourierdlem86  38886  fourierdlem94  38894  fourierdlem103  38903  fourierdlem104  38904  fourierdlem113  38913  hoidmvlelem1  39286  hoidmvlelem3  39288  hoidmvlelem4  39289  elfz0lmr  40191  nb3grpr  40609  frgr3v  41444  rngccatidALTV  41780  ringccatidALTV  41843
  Copyright terms: Public domain W3C validator