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

Theorem 3eqtr4i 2326
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1  |-  A  =  B
3eqtr4i.2  |-  C  =  A
3eqtr4i.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4i  |-  C  =  D

Proof of Theorem 3eqtr4i
StepHypRef Expression
1 3eqtr4i.2 . 2  |-  C  =  A
2 3eqtr4i.3 . . 3  |-  D  =  B
3 3eqtr4i.1 . . 3  |-  A  =  B
42, 3eqtr4i 2319 . 2  |-  D  =  A
51, 4eqtr4i 2319 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  rabswap  2732  rabbiia  2791  cbvrab  2799  cbvcsb  3098  csbco  3103  cbvrabcsf  3159  un4  3348  in13  3395  in31  3396  in4  3398  indifcom  3427  indir  3430  undir  3431  notrab  3458  dfnul3  3471  rab0  3488  dfif5  3590  prcom  3718  tprot  3735  tpcoma  3736  tpcomb  3737  tpass  3738  qdassr  3740  pw0  3778  pwpw0  3779  opid  3830  pwsn  3837  pwsnALT  3838  int0  3892  cbviun  3955  cbviin  3956  iunrab  3965  iunin1  3983  iinuni  4001  cbvopab  4103  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  cbvopab2v  4109  unopab  4111  cbvmpt  4126  iunopab  4312  dfid3  4326  uniuni  4543  rabxp  4741  fconstmpt  4748  resiundiOLD  4761  inxp  4834  cnvco  4881  rnmpt  4941  resundi  4985  resundir  4986  resindi  4987  resindir  4988  rescom  4996  resima  5003  imadmrn  5040  cnvimarndm  5050  cnvi  5101  cnvin  5104  rnun  5105  imaundi  5109  cnvxp  5113  imainrect  5135  imacnvcnv  5153  resdmres  5180  imadmres  5181  mptpreima  5182  cbviota  5240  sb8iota  5242  resdif  5510  fndmin  5648  zfrep6  5764  dfoprab2  5911  cbvoprab1  5934  cbvoprab2  5935  cbvoprab12  5936  cbvoprab3  5938  cbvmpt2x  5940  resoprab  5956  caov32  6063  caov31  6065  caov4  6067  caovlem2  6072  ofmres  6132  dfopab2  6190  dfxp3  6195  dmmpt2ssx  6205  fmpt2x  6206  fsplit  6239  ovtpos  6265  tposco  6281  opabiotadm  6308  cbvriota  6331  tfrlem10  6419  mapsncnv  6830  cbvixp  6849  xpcomco  6968  sbthlem6  6992  1sdom  7081  dfsup3OLD  7213  cardf2  7592  alephcard  7713  alephfplem1  7747  pwcda1  7836  ackbij1lem14  7875  compsscnv  8013  dffin1-5  8030  ituniiun  8064  axdc2lem  8090  axdc3lem4  8095  axcclem  8099  pwcfsdom  8221  dmaddpi  8530  dmmulpi  8531  adderpqlem  8594  addassnq  8598  mulcanenq  8600  addcmpblnr  8710  mulcmpblnrlem  8711  ltsrpr  8715  mulgt0sr  8743  sqgt0sr  8744  axi2m1  8797  negiso  9746  nummac  10172  fzprval  10860  fztpval  10861  seqval  11073  sqrecii  11202  sqdivi  11204  binom2i  11228  hashgval  11356  revs1  11499  cats1cat  11527  shftdm  11582  shftidt2  11592  cji  11660  cbvsum  12184  sumfc  12198  ackbijnn  12302  divalglem2  12610  bitsinv1lem  12648  nn0gcdsq  12839  prmreclem2  12980  prmrec  12985  hashbc0  13068  dec5nprm  13097  dec2nprm  13098  gcdi  13104  decexp2  13106  decsplit  13114  1259lem1  13145  1259lem4  13148  4001lem1  13155  strlemor2  13252  strlemor3  13253  phlstr  13303  oduval  14250  oduleval  14251  odubas  14253  oppgid  14845  gsumcom2  15242  rngidval  15359  oppr1  15432  dfrhm2  15514  ltbwe  16230  opsrtoslem1  16241  cnfldsub  16418  cnflddiv  16420  dvdsrz  16456  pjdm  16623  pjfval2  16625  restco  16911  cnmptid  17371  ufprim  17620  tgioo3  18327  oprpiece1res1  18465  oprpiece1res2  18466  volfiniun  18920  vitalilem4  18982  cbvitg  19146  itgresr  19149  iblcnlem1  19158  cbvditg  19220  sincos3rdpi  19900  ang180lem2  20124  1cubrlem  20153  asin1  20206  log2ublem2  20259  log2ublem3  20260  emcllem5  20309  lgsdir2lem5  20582  lgsquadlem3  20611  ex-un  20827  ex-pw  20832  ex-cnv  20840  ex-co  20841  bafval  21176  vsfval  21207  cnnvba  21263  cnnvm  21267  ip2dii  21438  siilem1  21445  h2hcau  21575  hvsubsub4i  21654  hvnegdii  21657  normlem3  21707  normlem8  21712  norm-iii-i  21734  normpar2i  21751  polid2i  21752  chjassi  22081  chj4i  22118  h1de2i  22148  spanunsni  22174  fh3i  22218  fh4i  22219  qlax4i  22225  qlaxr3i  22231  3oalem5  22261  pjadjii  22269  pjsubii  22273  hoadd32i  22374  cnvadj  22488  hh0oi  22499  hhcno  22500  hhcnf  22501  nmopnegi  22561  lnophmlem2  22613  branmfn  22701  ballotlem2  23063  ballotlemrinv  23108  abrexexd  23207  cbvmptf  23235  lmlimxrge0  23387  cbvesum  23437  unibrsiga  23532  subfacp1lem1  23725  kur14lem2  23753  kur14lem5  23756  kur14lem7  23758  cvmscld  23819  vdgrun  23908  vdegp1bi  23924  4bc2eq6  24114  cbvcprod  24137  prodfc  24171  predin  24260  predun  24261  preddif  24262  wfi  24278  frind  24314  symdifcom  24434  fixun  24520  ax5seglem7  24635  axlowdimlem4  24645  fsumcube  24867  rabiun2  24997  ovoliunnfl  25001  dfdir2  25394  cbvprodi  25415  fsumprd  25432  intopcoaconb  25643  selsubf  26093  selsubf3  26094  fninfp  26857  mendsca  27600  wallispilem4  27920  bnj1146  29139  bnj893  29276  bnj1234  29359  cdleme25cv  31169
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator