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

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

Proof of Theorem biid
StepHypRef Expression
1 id 22 . 2
21, 1impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  biidd  237  pm5.19  360  3anbi1i  1187  3anbi2i  1188  3anbi3i  1189  trubitru  1433  falbifal  1436  hadcoma  1455  hadcomb  1456  hadnot  1460  cadcomb  1463  eqid  2457  abid2  2597  abid2fOLD  2649  ceqsexg  3231  wecmpep  4876  sorpss  6585  ordon  6618  tz7.49c  7130  dford2  8058  infxpen  8413  isacn  8446  dfac5  8530  dfackm  8567  pwfseq  9063  axgroth5  9223  axgroth6  9227  supmul  10536  fsum2d  13586  cbvprod  13722  fprod2d  13785  rpnnen2  13959  isstruct  14642  oppccatid  15114  subccatid  15215  fuccatid  15338  setccatid  15411  catccatid  15429  xpccatid  15457  lubfun  15610  lubeldm  15611  lubelss  15612  lubval  15614  lubcl  15615  lubprop  15616  lublecl  15619  lubid  15620  glbfun  15623  glbeldm  15624  glbelss  15625  glbval  15627  glbcl  15628  glbprop  15629  joinval2  15639  joineu  15640  meetval2  15653  meeteu  15654  isglbd  15747  lubun  15753  meet0  15767  join0  15768  oduglb  15769  odulub  15771  poslubd  15778  symgsssg  16492  symgfisg  16493  pmtr3ncomlem1  16498  opprsubg  17285  abvtriv  17490  lmodvscl  17529  opsrtos  18150  iscnp2  19740  cbvditg  22258  ditgsplit  22265  lgsquad2  23635  nb3grapr  24453  frgra3v  25002  eqid1  25175  grpoidinv  25210  stri  27176  hstri  27184  stcltrthi  27197  nmo  27384  elxrge02  27628  toslub  27656  tosglb  27658  xrsclat  27668  slmdvscl  27757  sgnneg  28479  cvmliftlem11  28740  socnv  29194  dfon2  29224  sltsolem1  29428  brpprod3b  29537  brapply  29588  brrestrict  29599  dfrdg4  29600  cgr3permute3  29697  cgr3permute1  29698  cgr3permute2  29699  cgr3permute4  29700  cgr3permute5  29701  colinearxfr  29725  brsegle  29758  wl-equsal1t  29994  bicontr  30477  rngunsnply  31122  iotaequ  31336  ioodvbdlimc1  31730  ioodvbdlimc2  31732  fourierdlem86  31975  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  ismgmhm  32471  estrccatid  32638  rngccatidOLD  32797  ringccatidOLD  32860  2uasban  33335  uunT1  33577  e2ebindVD  33712  e2ebindALT  33729  iunconALT  33736  bnj1383  33890  bnj1386  33892  bnj153  33938  bnj543  33951  bnj544  33952  bnj546  33954  bnj605  33965  bnj579  33972  bnj600  33977  bnj601  33978  bnj852  33979  bnj893  33986  bnj906  33988  bnj917  33992  bnj938  33995  bnj944  33996  bnj998  34014  bnj1006  34017  bnj1029  34024  bnj1034  34026  bnj1124  34044  bnj1128  34046  bnj1127  34047  bnj1125  34048  bnj1147  34050  bnj1190  34064  bnj69  34066  bnj1204  34068  bnj1311  34080  bnj1318  34081  bnj1384  34088  bnj1408  34092  bnj1414  34093  bnj1415  34094  bnj1421  34098  bnj1423  34107  bnj1489  34112  bnj1493  34115  bnj60  34118  bnj1500  34124  bnj1522  34128  bj-abid2  34368  bj-termab  34421  lub0N  34914  glb0N  34918  glbconN  35101  dalemeea  35387  dalem4  35389  dalem6  35392  dalem7  35393  dalem11  35398  dalem12  35399  dalem29  35425  dalem30  35426  dalem31N  35427  dalem32  35428  dalem33  35429  dalem34  35430  dalem35  35431  dalem36  35432  dalem37  35433  dalem40  35436  dalem46  35442  dalem47  35443  dalem49  35445  dalem50  35446  dalem52  35448  dalem53  35449  dalem54  35450  dalem56  35452  dalem58  35454  dalem59  35455  dalem62  35458  paddval  35522  4atexlemex4  35797  4atexlemex6  35798  cdleme31sdnN  36113  cdlemefr44  36151  cdleme48fv  36225  cdlemeg49lebilem  36265  cdleme50eq  36267  axfrege54a  37888
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 185
  Copyright terms: Public domain W3C validator