MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtri Structured version   Visualization version   GIF version

Theorem 3eqtri 2635
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1 𝐴 = 𝐵
3eqtri.2 𝐵 = 𝐶
3eqtri.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtri 𝐴 = 𝐷

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2 𝐴 = 𝐵
2 3eqtri.2 . . 3 𝐵 = 𝐶
3 3eqtri.3 . . 3 𝐶 = 𝐷
42, 3eqtri 2631 . 2 𝐵 = 𝐷
51, 4eqtri 2631 1 𝐴 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  csbid  3506  un23  3733  in32  3786  unvdif  3993  undif2  3995  undifabs  3996  difun2  3999  difdifdir  4007  dfif4  4050  dfif5  4051  tpidm23  4235  dfopif  4331  unisn  4381  dfiunv2  4486  symdif0  4527  symdifid  4529  unidif0  4759  uniop  4893  xpun  5089  dfrn2  5221  dfdmf  5226  dfrnf  5272  res0  5308  resres  5316  xpssres  5341  dfima2  5374  imai  5384  ima0  5387  imaundir  5451  xpima  5481  dmresv  5497  rescnvcnv  5501  dmtpop  5515  rnsnopg  5518  resdmres  5529  dmmpt  5533  dmco  5546  co01  5553  suc0  5702  unisuc  5704  iunsuc  5710  fresaun  5973  dffv4  6085  fvssunirn  6112  fpr  6304  fvsnun2  6332  mpt20  6601  dmoprab  6617  rnoprab  6619  elrnmpt2res  6650  ov6g  6674  1st0  7042  2nd0  7043  dfmpt2  7131  curry1  7133  curry2  7136  fpar  7145  algrflem  7150  dftpos2  7233  tposoprab  7252  tposmpt2  7253  fvmpt2curryd  7261  wfrlem14  7292  wfrlem16  7294  dfrecs3  7333  tfrlem8  7344  seqomlem3  7411  df2o3  7437  omxpenlem  7923  dfsdom2  7945  marypha2lem2  8202  scottexs  8610  scott0s  8611  infxpenc2  8705  kmlem3  8834  cdaassen  8864  ackbij1lem2  8903  compsscnv  9053  fin1a2lem12  9093  mulerpqlem  9633  1lt2nq  9651  axi2m1  9836  2p2e4  10991  numsuc  11343  numsucc  11381  decmul10add  11425  decmul10addOLD  11426  5p5e10  11428  6p4e10  11430  7p3e10  11435  xnegmnf  11874  pnfaddmnf  11894  fz0tp  12264  fz0to3un2pr  12265  fzo13pr  12374  fzo0to2pr  12375  fzo0to3tp  12376  fzo0to42pr  12377  fzo1to4tp  12378  sq4e2t8  12779  i4  12784  crreczi  12806  fac1  12881  fac3  12884  hashkf  12936  hashinf  12939  dmhashres  12943  hashun3  12986  cshwsexa  13367  dmtrclfv  13553  abs0  13819  absi  13820  trirecip  14380  geoihalfsum  14399  esum  14596  tan0  14666  coshval  14670  ef01bndlem  14699  3dvds  14836  3dvdsOLD  14837  3dvdsdec  14838  3dvdsdecOLD  14839  3dvds2dec  14840  3dvds2decOLD  14841  sadc0  14960  3lcm2e6woprm  15112  6lcm4e12  15113  lcmf0  15131  prmo0  15524  gcdmodi  15562  karatsuba  15576  karatsubaOLD  15577  43prm  15613  139prm  15615  631prm  15618  1259lem1  15622  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  2503lem1  15628  2503lem2  15629  2503lem3  15630  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  ndxarg  15661  setsfun  15671  setsfun0  15672  xpsc  15986  pmtrsn  17708  psgnprfval1  17711  sylow2a  17803  0frgp  17961  ablfac1eu  18241  sralem  18944  opsrtoslem2  19252  ply1plusgfvi  19379  pf1rcl  19480  restcld  20728  neitr  20736  txbasval  21161  txindis  21189  cnmpt1st  21223  cnmpt2nd  21224  ufildr  21487  restmetu  22126  reust  22894  ismbl  23018  mbfimaopnlem  23145  itg10  23178  itg2cnlem2  23252  itgz  23270  dvmptid  23443  cos2pi  23949  tan4thpi  23987  sincos6thpi  23988  pige3  23990  dfrelog  24033  logm1  24056  dvlog  24114  efopnlem2  24120  cxpexp  24131  root1id  24212  ang180lem2  24257  1cubrlem  24285  quart1  24300  atandm2  24321  efiasin  24332  asinsinlem  24335  asinsin  24336  asin1  24338  acos1  24339  atancj  24354  atanlogsublem  24359  efiatan2  24361  2efiatan  24362  tanatan  24363  dvatan  24379  log2cnv  24388  log2ublem2  24391  log2ublem3  24392  basellem8  24531  cht1  24608  chp1  24610  ppi1i  24611  ppi2i  24612  cht2  24615  cht3  24616  bclbnd  24722  bposlem8  24733  2lgslem3c  24840  2lgslem3d  24841  ax5seglem7  25533  axlowdimlem8  25547  axlowdimlem11  25550  wlkntrllem2  25856  constr1trl  25884  constr2spthlem1  25890  constr3trllem3  25946  constr3pthlem1  25949  constr3pthlem3  25951  wlknwwlknvbij  26034  clwwlkvbij  26095  vdegp1ai  26277  ex-dif  26438  ex-xp  26451  ex-rn  26455  ex-lcm  26473  ex-prmo  26474  ip0i  26870  ip1ilem  26871  ipdirilem  26874  ipasslem10  26884  hvnegdii  27109  hvaddcani  27112  hvsubaddi  27113  hisubcomi  27151  normlem0  27156  normlem3  27159  normlem9  27165  bcseqi  27167  norm0  27175  norm-ii-i  27184  norm3difi  27194  normpari  27201  normpar2i  27203  polid2i  27204  shs0i  27498  chj0i  27504  pjsslem  27728  ho0subi  27844  hoaddsubi  27870  hosd1i  27871  hopncani  27873  nmop0  28035  nmfn0  28036  lnopunilem1  28059  lnophmlem2  28066  opsqrlem2  28190  pjclem1  28244  atabsi  28450  dmdbr6ati  28472  inin  28543  iuninc  28567  gtiso  28667  fpwrelmapffs  28703  lmat22det  29022  ordtcnvNEW  29100  ordtrest2NEW  29103  zlmtset  29143  qqhucn  29170  zrhre  29197  qqhre  29198  esumnul  29243  mbfmcst  29454  carsggect  29513  eulerpartgbij  29567  eulerpartlemn  29576  fib0  29594  fib1  29595  fib2  29597  fib3  29598  fib4  29599  fib5  29600  fib6  29601  0rrv  29646  coinflipprob  29674  ballotlem2  29683  ballotth  29732  signsvf0  29789  bnj1416  30167  derang0  30211  subfac0  30219  subfac1  30220  mthmpps  30539  problem2  30619  problem2OLD  30620  quad3  30624  dfrdg2  30751  trpred0  30786  pprodcnveq  30966  dffv5  31007  fullfunfv  31030  ellines  31235  rankeq1o  31254  onint1  31424  bj-xpimasn  31931  bj-pr11val  31982  bj-pr21val  31990  bj-pr22val  31996  bj-nuliotaALT  32007  bj-dfmpt2a  32048  icorempt2  32171  finxpreclem4  32203  finxp2o  32208  finxp3o  32209  matunitlindf  32373  poimirlem5  32380  poimirlem22  32397  poimirlem26  32401  poimirlem30  32405  ismblfin  32416  dvtan  32426  asindmre  32461  dvasin  32462  dvacos  32463  areacirclem5  32470  heiborlem6  32581  hdmap1cbv  35906  diophrw  36136  dnwech  36432  lmhmlnmsplit  36471  fgraphopab  36603  arearect  36616  areaquad  36617  dmnonrel  36711  imanonrel  36714  cononrel1  36715  cononrel2  36716  rclexi  36737  dfrtrcl5  36751  cnvtrrel  36777  dfrcl2  36781  dfrcl4  36783  iunrelexp0  36809  comptiunov2i  36813  relexpaddss  36825  brtrclfv2  36834  trclfvdecomr  36835  corcltrcl  36846  cotrclrcl  36849  fsovcnvlem  37123  neicvgnvo  37229  hashnzfz  37337  lhe4.4ex1a  37346  disjinfi  38171  tgqioo2  38418  sumnnodd  38494  cosnegpi  38547  itgsin0pilem1  38638  stoweidlem13  38703  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem3  38766  dirkertrigeqlem1  38788  fourierdlem56  38852  fourierdlem57  38853  fourierdlem58  38854  fourierdlem62  38858  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  sqwvfoura  38918  fouriersw  38921  etransclem23  38947  etransclem36  38960  etransclem38  38962  carageniuncllem1  39208  0ome  39216  ovn02  39255  smflimlem4  39457  smflim  39460  fmtno0  39788  fmtno1  39789  fmtno2  39798  fmtno3  39799  fmtno4  39800  fmtno5lem4  39804  139prmALT  39847  31prm  39848  5tcu2e40  39868  3exp4mod41  39869  41prothprmlem2  39871  41prothprm  39872  nnsum3primesgbe  40006  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  bgoldbtbndlem1  40019  tgoldbachlt  40028  tgoldbachltOLD  40035  umgrislfupgrlem  40342  usgrexmpledg  40481  vdegp1bi-av  40748  uhgr1wlkspthlem2  40955  wlksnwwlknvbij  41109  clwwlksvbij  41224  1wlk2v2elem2  41318  cznrnglem  41740  2t6m3t4e0  41914  zlmodzxzldeplem3  42080  sec0  42256
  Copyright terms: Public domain W3C validator