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

Theorem 3eqtr4i 2313
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 2306 . 2  |-  D  =  A
51, 4eqtr4i 2306 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  rabswap  2719  rabbiia  2778  cbvrab  2786  cbvcsb  3085  csbco  3090  cbvrabcsf  3146  un4  3335  in13  3382  in31  3383  in4  3385  indifcom  3414  indir  3417  undir  3418  notrab  3445  dfnul3  3458  rab0  3475  dfif5  3577  prcom  3705  tprot  3722  tpcoma  3723  tpcomb  3724  tpass  3725  qdassr  3727  pw0  3762  pwpw0  3763  opid  3814  pwsn  3821  pwsnALT  3822  int0  3876  cbviun  3939  cbviin  3940  iunrab  3949  iunin1  3967  iinuni  3985  cbvopab  4087  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  cbvopab2v  4093  unopab  4095  cbvmpt  4110  iunopab  4296  dfid3  4310  uniuni  4527  rabxp  4725  fconstmpt  4732  resiundiOLD  4745  inxp  4818  cnvco  4865  rnmpt  4925  resundi  4969  resundir  4970  resindi  4971  resindir  4972  rescom  4980  resima  4987  imadmrn  5024  cnvimarndm  5034  cnvi  5085  cnvin  5088  rnun  5089  imaundi  5093  cnvxp  5097  imainrect  5119  imacnvcnv  5137  resdmres  5164  imadmres  5165  mptpreima  5166  cbviota  5224  sb8iota  5226  resdif  5494  fndmin  5632  zfrep6  5748  dfoprab2  5895  cbvoprab1  5918  cbvoprab2  5919  cbvoprab12  5920  cbvoprab3  5922  cbvmpt2x  5924  resoprab  5940  caov32  6047  caov31  6049  caov4  6051  caovlem2  6056  ofmres  6116  dfopab2  6174  dfxp3  6179  dmmpt2ssx  6189  fmpt2x  6190  fsplit  6223  ovtpos  6249  tposco  6265  opabiotadm  6292  cbvriota  6315  tfrlem10  6403  mapsncnv  6814  cbvixp  6833  xpcomco  6952  sbthlem6  6976  1sdom  7065  dfsup3OLD  7197  cardf2  7576  alephcard  7697  alephfplem1  7731  pwcda1  7820  ackbij1lem14  7859  compsscnv  7997  dffin1-5  8014  ituniiun  8048  axdc2lem  8074  axdc3lem4  8079  axcclem  8083  pwcfsdom  8205  dmaddpi  8514  dmmulpi  8515  adderpqlem  8578  addassnq  8582  mulcanenq  8584  addcmpblnr  8694  mulcmpblnrlem  8695  ltsrpr  8699  mulgt0sr  8727  sqgt0sr  8728  axi2m1  8781  negiso  9730  nummac  10156  fzprval  10844  fztpval  10845  seqval  11057  sqrecii  11186  sqdivi  11188  binom2i  11212  hashgval  11340  revs1  11483  cats1cat  11511  shftdm  11566  shftidt2  11576  cji  11644  cbvsum  12168  sumfc  12182  ackbijnn  12286  divalglem2  12594  bitsinv1lem  12632  nn0gcdsq  12823  prmreclem2  12964  prmrec  12969  hashbc0  13052  dec5nprm  13081  dec2nprm  13082  gcdi  13088  decexp2  13090  decsplit  13098  1259lem1  13129  1259lem4  13132  4001lem1  13139  strlemor2  13236  strlemor3  13237  phlstr  13287  oduval  14234  oduleval  14235  odubas  14237  oppgid  14829  gsumcom2  15226  rngidval  15343  oppr1  15416  dfrhm2  15498  ltbwe  16214  opsrtoslem1  16225  cnfldsub  16402  cnflddiv  16404  dvdsrz  16440  pjdm  16607  pjfval2  16609  restco  16895  cnmptid  17355  ufprim  17604  tgioo3  18311  oprpiece1res1  18449  oprpiece1res2  18450  volfiniun  18904  vitalilem4  18966  cbvitg  19130  itgresr  19133  iblcnlem1  19142  cbvditg  19204  sincos3rdpi  19884  ang180lem2  20108  1cubrlem  20137  asin1  20190  log2ublem2  20243  log2ublem3  20244  emcllem5  20293  lgsdir2lem5  20566  lgsquadlem3  20595  ex-un  20811  ex-pw  20816  ex-cnv  20824  ex-co  20825  bafval  21160  vsfval  21191  cnnvba  21247  cnnvm  21251  ip2dii  21422  siilem1  21429  h2hcau  21559  hvsubsub4i  21638  hvnegdii  21641  normlem3  21691  normlem8  21696  norm-iii-i  21718  normpar2i  21735  polid2i  21736  chjassi  22065  chj4i  22102  h1de2i  22132  spanunsni  22158  fh3i  22202  fh4i  22203  qlax4i  22209  qlaxr3i  22215  3oalem5  22245  pjadjii  22253  pjsubii  22257  hoadd32i  22358  cnvadj  22472  hh0oi  22483  hhcno  22484  hhcnf  22485  nmopnegi  22545  lnophmlem2  22597  branmfn  22685  ballotlem2  23047  ballotlemrinv  23092  subfacp1lem1  23121  kur14lem2  23149  kur14lem5  23152  kur14lem7  23154  cvmscld  23215  vdgrun  23304  vdegp1bi  23320  4bc2eq6  23510  predin  23600  predun  23601  preddif  23602  wfi  23618  frind  23654  symdifcom  23774  fixun  23860  ax5seglem7  23974  axlowdimlem4  23984  fsumcube  24206  dfdir2  24703  cbvprodi  24724  fsumprd  24741  intopcoaconb  24952  selsubf  25402  selsubf3  25403  fninfp  26166  mendsca  26909  wallispilem4  27229  bnj1146  28196  bnj893  28333  bnj1234  28416  cdleme25cv  29920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator