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

Theorem 3eqtr4i 2434
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 2427 . 2  |-  D  =  A
51, 4eqtr4i 2427 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  rabswap  2847  rabbiia  2906  cbvrab  2914  cbvcsb  3215  csbco  3220  cbvrabcsf  3274  un4  3467  in13  3514  in31  3515  in4  3517  indifcom  3546  indir  3549  undir  3550  difdif2  3558  notrab  3578  dfnul3  3591  rab0  3608  dfif5  3711  prcom  3842  tprot  3859  tpcoma  3860  tpcomb  3861  tpass  3862  qdassr  3864  pw0  3905  pwpw0  3906  opid  3962  pwsn  3969  pwsnALT  3970  int0  4024  cbviun  4088  cbviin  4089  iunrab  4098  iunin1  4116  iinuni  4134  cbvopab  4236  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  cbvopab2v  4242  unopab  4244  cbvmpt  4259  iunopab  4446  dfid3  4459  uniuni  4675  rabxp  4873  fconstmpt  4880  inxp  4966  cnvco  5015  rnmpt  5075  resundi  5119  resundir  5120  resindi  5121  resindir  5122  rescom  5130  resima  5137  imadmrn  5174  cnvimarndm  5184  cnvi  5235  cnvin  5238  rnun  5239  imaundi  5243  cnvxp  5249  imainrect  5271  imacnvcnv  5293  resdmres  5320  imadmres  5321  mptpreima  5322  cbviota  5382  sb8iota  5384  resdif  5655  fndmin  5796  zfrep6  5927  dfoprab2  6080  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab3  6107  cbvmpt2x  6109  resoprab  6125  caov32  6233  caov31  6235  caov4  6237  caovlem2  6242  ofmres  6302  dfopab2  6360  dfxp3  6365  dmmpt2ssx  6375  fmpt2x  6376  fsplit  6410  ovtpos  6453  tposco  6469  opabiotadm  6496  cbvriota  6519  tfrlem10  6607  mapsncnv  7019  cbvixp  7038  xpcomco  7157  sbthlem6  7181  1sdom  7270  dfsup3OLD  7407  cardf2  7786  alephcard  7907  alephfplem1  7941  pwcda1  8030  ackbij1lem14  8069  compsscnv  8207  dffin1-5  8224  ituniiun  8258  axdc2lem  8284  axdc3lem4  8289  axcclem  8293  pwcfsdom  8414  dmaddpi  8723  dmmulpi  8724  adderpqlem  8787  addassnq  8791  mulcanenq  8793  addcmpblnr  8903  mulcmpblnrlem  8904  ltsrpr  8908  mulgt0sr  8936  sqgt0sr  8937  axi2m1  8990  negiso  9940  nummac  10370  fzprval  11062  fztpval  11063  seqval  11289  sqrecii  11419  sqdivi  11421  binom2i  11445  hashgval  11576  revs1  11752  cats1cat  11780  shftdm  11841  shftidt2  11851  cji  11919  cbvsum  12444  sumfc  12458  ackbijnn  12562  divalglem2  12870  nn0gcdsq  13099  prmreclem2  13240  prmrec  13245  hashbc0  13328  dec5nprm  13357  dec2nprm  13358  gcdi  13364  decexp2  13366  decsplit  13374  1259lem1  13405  1259lem4  13408  4001lem1  13415  strlemor2  13512  strlemor3  13513  phlstr  13563  oduval  14512  oduleval  14513  odubas  14515  oppgid  15107  gsumcom2  15504  rngidval  15621  oppr1  15694  dfrhm2  15776  ltbwe  16488  opsrtoslem1  16499  cnfldsub  16684  cnflddiv  16686  dvdsrz  16722  pjdm  16889  pjfval2  16891  restco  17182  cnmptid  17646  ufprim  17894  tgioo3  18789  oprpiece1res1  18929  oprpiece1res2  18930  volfiniun  19394  vitalilem4  19456  cbvitg  19620  itgresr  19623  iblcnlem1  19632  cbvditg  19694  sincos3rdpi  20377  ang180lem2  20605  1cubrlem  20634  asin1  20687  log2ublem2  20740  log2ublem3  20741  emcllem5  20791  lgsdir2lem5  21064  lgsquadlem3  21093  usgrafilem1  21378  cusgrasizeindslem2  21436  vdgrun  21625  vdgrfiun  21626  vdegp1bi  21660  ex-un  21685  ex-pw  21690  ex-cnv  21698  ex-co  21699  bafval  22036  vsfval  22067  cnnvba  22123  cnnvm  22127  ip2dii  22298  siilem1  22305  h2hcau  22435  hvsubsub4i  22514  hvnegdii  22517  normlem3  22567  normlem8  22572  norm-iii-i  22594  normpar2i  22611  polid2i  22612  chjassi  22941  chj4i  22978  h1de2i  23008  spanunsni  23034  fh3i  23078  fh4i  23079  qlax4i  23085  qlaxr3i  23091  3oalem5  23121  pjadjii  23129  pjsubii  23133  hoadd32i  23234  cnvadj  23348  hh0oi  23359  hhcno  23360  hhcnf  23361  nmopnegi  23421  lnophmlem2  23473  branmfn  23561  abrexexd  23943  cbvmptf  24021  lmlimxrge0  24287  rrhre  24340  cbvesum  24391  unibrsiga  24493  ballotlem2  24699  ballotlemrinv  24744  subfacp1lem1  24818  kur14lem2  24846  kur14lem5  24849  kur14lem7  24851  cvmscld  24913  dfid4  25136  4bc2eq6  25157  cbvprod  25194  prodfc  25224  predin  25403  predun  25404  preddif  25405  wfi  25421  frind  25457  symdifcom  25577  fixun  25663  ax5seglem7  25778  axlowdimlem4  25788  fsumcube  26010  rabiun2  26139  ovoliunnfl  26147  voliunnfl  26149  mbfposadd  26153  fninfp  26625  mendsca  27365  stoweidlem13  27629  wallispilem4  27684  bnj1146  28868  bnj893  29005  bnj1234  29088  cdleme25cv  30840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator