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

Theorem biid 229
Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
biid

Proof of Theorem biid
StepHypRef Expression
1 id 21 . 2
21, 1impbii 182 1
Colors of variables: wff set class
Syntax hints:  <->wb 178
This theorem is referenced by:  biidd  230  pm5.19  351  3anbi1i  1145  3anbi2i  1146  3anbi3i  1147  trujust  1328  tru  1331  trubitru  1360  falbifal  1363  hadcoma  1398  hadcomb  1399  hadnot  1403  cadcomb  1406  eqid  2447  abid2  2564  abid2f  2608  ceqsexg  3080  wecmpep  4619  ordon  4808  sorpss  6581  tz7.49c  6756  dford2  7628  infxpen  7951  isacn  7980  dfac5  8064  dfackm  8101  pwfseq  8594  axgroth5  8754  axgroth6  8758  supmul  10031  fsum2d  12610  rpnnen2  12880  isstruct  13534  oppccatid  14000  subccatid  14098  fuccatid  14221  setccatid  14294  catccatid  14312  xpccatid  14340  opprsubg  15777  abvtriv  15965  lmodvscl  16003  opsrtos  16582  iscnp2  17339  cbvditg  19777  ditgsplit  19784  lgsquad2  21180  nb3grapr  21498  eqid1  21797  grpoidinv  21832  stri  23796  hstri  23804  stcltrthi  23817  nmo  24011  elxrge02  24254  slmdvscl  24391  cvmliftlem11  25242  cbvprod  25501  fprod2d  25565  socnv  25648  dfon2  25679  sltsolem1  25883  brpprod3b  25992  brapply  26043  brrestrict  26054  dfrdg4  26055  cgr3permute3  26241  cgr3permute1  26242  cgr3permute2  26243  cgr3permute4  26244  cgr3permute5  26245  colinearxfr  26269  brsegle  26302  bicontr  26957  rngunsnply  27690  symgsssg  27720  symgfisg  27721  iotaequ  27941  frgra3v  28786  2uasban  29044  e2ebindVD  29421  e2ebindALT  29438  iunconALT  29445  bnj1383  29600  bnj1386  29602  bnj153  29648  bnj543  29661  bnj544  29662  bnj546  29664  bnj605  29675  bnj579  29682  bnj600  29687  bnj601  29688  bnj852  29689  bnj893  29696  bnj906  29698  bnj917  29702  bnj938  29705  bnj944  29706  bnj998  29724  bnj1006  29727  bnj1029  29734  bnj1034  29736  bnj1124  29754  bnj1128  29756  bnj1127  29757  bnj1125  29758  bnj1147  29760  bnj1190  29774  bnj69  29776  bnj1204  29778  bnj1311  29790  bnj1318  29791  bnj1384  29798  bnj1408  29802  bnj1414  29803  bnj1415  29804  bnj1421  29808  bnj1423  29817  bnj1489  29822  bnj1493  29825  bnj60  29828  bnj1500  29834  bnj1522  29838  dalemeea  30856  dalem4  30858  dalem6  30861  dalem7  30862  dalem11  30867  dalem12  30868  dalem29  30894  dalem30  30895  dalem31N  30896  dalem32  30897  dalem33  30898  dalem34  30899  dalem35  30900  dalem36  30901  dalem37  30902  dalem40  30905  dalem46  30911  dalem47  30912  dalem49  30914  dalem50  30915  dalem52  30917  dalem53  30918  dalem54  30919  dalem56  30921  dalem58  30923  dalem59  30924  dalem62  30927  paddval  30991  4atexlemex4  31266  4atexlemex6  31267  cdleme31sdnN  31580  cdlemefr44  31618  cdleme48fv  31692  cdlemeg49lebilem  31732  cdleme50eq  31734
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 179
  Copyright terms: Public domain W3C validator