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

Theorem 3eqtr4i 2465
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 2458 . 2  |-  D  =  A
51, 4eqtr4i 2458 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  rabswap  2879  rabbiia  2938  cbvrab  2946  cbvcsb  3247  csbco  3252  cbvrabcsf  3306  un4  3499  in13  3546  in31  3547  in4  3549  indifcom  3578  indir  3581  undir  3582  difdif2  3590  notrab  3610  dfnul3  3623  rab0  3640  dfif5  3743  prcom  3874  tprot  3891  tpcoma  3892  tpcomb  3893  tpass  3894  qdassr  3896  pw0  3937  pwpw0  3938  opid  3994  pwsn  4001  pwsnALT  4002  int0  4056  cbviun  4120  cbviin  4121  iunrab  4130  iunin1  4148  iinuni  4166  cbvopab  4268  cbvopab1  4270  cbvopab2  4271  cbvopab1s  4272  cbvopab2v  4274  unopab  4276  cbvmpt  4291  iunopab  4478  dfid3  4491  uniuni  4708  rabxp  4906  fconstmpt  4913  inxp  4999  cnvco  5048  rnmpt  5108  resundi  5152  resundir  5153  resindi  5154  resindir  5155  rescom  5163  resima  5170  imadmrn  5207  cnvimarndm  5217  cnvi  5268  cnvin  5271  rnun  5272  imaundi  5276  cnvxp  5282  imainrect  5304  imacnvcnv  5326  resdmres  5353  imadmres  5354  mptpreima  5355  cbviota  5415  sb8iota  5417  resdif  5688  fndmin  5829  zfrep6  5960  dfoprab2  6113  cbvoprab1  6136  cbvoprab2  6137  cbvoprab12  6138  cbvoprab3  6140  cbvmpt2x  6142  resoprab  6158  caov32  6266  caov31  6268  caov4  6270  caovlem2  6275  ofmres  6335  dfopab2  6393  dfxp3  6398  dmmpt2ssx  6408  fmpt2x  6409  fsplit  6443  ovtpos  6486  tposco  6502  opabiotadm  6529  cbvriota  6552  tfrlem10  6640  mapsncnv  7052  cbvixp  7071  xpcomco  7190  sbthlem6  7214  1sdom  7303  dfsup3OLD  7441  cardf2  7822  alephcard  7943  alephfplem1  7977  pwcda1  8066  ackbij1lem14  8105  compsscnv  8243  dffin1-5  8260  ituniiun  8294  axdc2lem  8320  axdc3lem4  8325  axcclem  8329  pwcfsdom  8450  dmaddpi  8759  dmmulpi  8760  adderpqlem  8823  addassnq  8827  mulcanenq  8829  addcmpblnr  8939  mulcmpblnrlem  8940  ltsrpr  8944  mulgt0sr  8972  sqgt0sr  8973  axi2m1  9026  negiso  9976  nummac  10406  fzprval  11098  fztpval  11099  seqval  11326  sqrecii  11456  sqdivi  11458  binom2i  11482  hashgval  11613  revs1  11789  cats1cat  11817  shftdm  11878  shftidt2  11888  cji  11956  cbvsum  12481  sumfc  12495  ackbijnn  12599  divalglem2  12907  nn0gcdsq  13136  prmreclem2  13277  prmrec  13282  hashbc0  13365  dec5nprm  13394  dec2nprm  13395  gcdi  13401  decexp2  13403  decsplit  13411  1259lem1  13442  1259lem4  13445  4001lem1  13452  strlemor2  13549  strlemor3  13550  phlstr  13600  oduval  14549  oduleval  14550  odubas  14552  oppgid  15144  gsumcom2  15541  rngidval  15658  oppr1  15731  dfrhm2  15813  ltbwe  16525  opsrtoslem1  16536  cnfldsub  16721  cnflddiv  16723  dvdsrz  16759  pjdm  16926  pjfval2  16928  restco  17220  cnmptid  17685  ufprim  17933  tgioo3  18828  oprpiece1res1  18968  oprpiece1res2  18969  volfiniun  19433  vitalilem4  19495  cbvitg  19659  itgresr  19662  iblcnlem1  19671  cbvditg  19733  sincos3rdpi  20416  ang180lem2  20644  1cubrlem  20673  asin1  20726  log2ublem2  20779  log2ublem3  20780  emcllem5  20830  lgsdir2lem5  21103  lgsquadlem3  21132  usgrafilem1  21417  cusgrasizeindslem2  21475  vdgrun  21664  vdgrfiun  21665  vdegp1bi  21699  ex-un  21724  ex-pw  21729  ex-cnv  21737  ex-co  21738  bafval  22075  vsfval  22106  cnnvba  22162  cnnvm  22166  ip2dii  22337  siilem1  22344  h2hcau  22474  hvsubsub4i  22553  hvnegdii  22556  normlem3  22606  normlem8  22611  norm-iii-i  22633  normpar2i  22650  polid2i  22651  chjassi  22980  chj4i  23017  h1de2i  23047  spanunsni  23073  fh3i  23117  fh4i  23118  qlax4i  23124  qlaxr3i  23130  3oalem5  23160  pjadjii  23168  pjsubii  23172  hoadd32i  23273  cnvadj  23387  hh0oi  23398  hhcno  23399  hhcnf  23400  nmopnegi  23460  lnophmlem2  23512  branmfn  23600  abrexexd  23982  cbvmptf  24060  lmlimxrge0  24326  rrhre  24379  cbvesum  24430  unibrsiga  24532  ballotlem2  24738  ballotlemrinv  24783  subfacp1lem1  24857  kur14lem2  24885  kur14lem5  24888  kur14lem7  24890  cvmscld  24952  dfid4  25175  4bc2eq6  25196  cbvprod  25233  prodfc  25263  predin  25456  predun  25457  preddif  25458  wfi  25474  frind  25510  symdifcom  25656  fixun  25746  ax5seglem7  25866  axlowdimlem4  25876  fsumcube  26098  rabiun2  26230  ovoliunnfl  26238  voliunnfl  26240  mbfposadd  26244  fninfp  26726  mendsca  27465  stoweidlem13  27729  wallispilem4  27784  bnj1146  29099  bnj893  29236  bnj1234  29319  cdleme25cv  31092
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator