Theorem 3eqtri 2756

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

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3		3eqtri.3	. . 3 ⊢ 𝐶 = 𝐷
4	2, 3	eqtri 2752	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2752	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  csbid  3866  csbconstg  3872  csbie  3888  un23  4127  in32  4183  dfnul4  4288  unvdif  4428  undif2  4430  undifabs  4431  difun2  4434  difdifdir  4445  dfif4  4494  dfif5  4495  tpidm23  4711  dfopif  4824  dfiunv2  4987  symdif0  5037  symdifid  5039  unidif0  5302  uniop  5462  xpun  5697  dfrn2  5835  dfdmf  5843  dfrnf  5896  res0  5938  resres  5947  xpssres  5973  dfima2  6017  imai  6029  ima0  6032  imaundir  6103  xpima  6135  cnvrescnv  6148  dmresv  6153  rescnvcnv  6157  dmtpop  6171  rnsnopg  6174  resdmres  6185  resdifdi  6189  dmmpt  6193  dmco  6207  co01  6214  suc0  6388  iunsuc  6398  fresaun  6699  dffv4  6823  fvssunirnOLD  6858  f1ossf1o  7066  fpr  7092  mpo0  7438  dmoprab  7456  rnoprab  7458  elrnmpores  7491  ov6g  7517  1st0  7937  2nd0  7938  dfmpo  8042  curry1  8044  curry2  8047  fpar  8056  dftpos2  8183  tposoprab  8202  tposmpo  8203  fvmpocurryd  8211  frrlem14  8239  dfrecs3  8302  tfrlem8  8313  seqomlem3  8381  df2o3  8403  nlim2  8415  omxpenlem  9002  dfsdom2  9024  pwfir  9224  marypha2lem2  9345  sup00  9374  epinid0  9514  scottexs  9802  scott0s  9803  infxpenc2  9935  kmlem3  10066  ackbij1lem2  10133  compsscnv  10284  fin1a2lem12  10324  mulerpqlem  10868  1lt2nq  10886  axi2m1  11072  2p2e4  12276  numsuc  12623  numsucc  12649  decmul10add  12678  5p5e10  12680  6p4e10  12681  7p3e10  12684  xnegmnf  13130  pnfaddmnf  13150  fz12pr  13502  fz0tp  13549  fz0to3un2pr  13550  fz0to4untppr  13551  fz0to5un2tp  13552  fzo13pr  13670  fzo0to2pr  13671  fz01pr  13672  fzo0to3tp  13673  fzo0to42pr  13674  fzo1to4tp  13675  fldiv4p1lem1div2  13757  sq4e2t8  14124  i4  14129  crreczi  14153  fac1  14202  fac3  14205  hashkf  14257  hashinf  14260  dmhashres  14266  hashun3  14309  cshwsexaOLD  14749  dmtrclfv  14943  abs0  15210  absi  15211  trirecip  15788  geoihalfsum  15807  esum  16005  tan0  16078  coshval  16082  ef01bndlem  16111  3dvds  16260  3dvdsdec  16261  3dvds2dec  16262  sadc0  16383  3lcm2e6woprm  16544  6lcm4e12  16545  lcmf0  16563  prmo0  16966  gcdmodi  17004  karatsuba  17013  43prm  17051  139prm  17053  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  setsfun  17100  setsfun0  17101  ndxarg  17125  pmtrsn  19416  psgnprfval1  19419  sylow2a  19516  ablfac1eu  19972  sralem  21098  pzriprng1ALT  21421  opsrtoslem2  21979  ply1plusgfvi  22142  pf1rcl  22252  restcld  23075  neitr  23083  txbasval  23509  txindis  23537  cnmpt1st  23571  cnmpt2nd  23572  ufildr  23834  restmetu  24474  cphipval2  25157  reust  25297  ehl0base  25332  ismbl  25443  mbfimaopnlem  25572  itg10  25605  itg2cnlem2  25679  itgz  25698  dvmptid  25877  cos2pi  26401  tan4thpi  26439  tan4thpiOLD  26440  sincos6thpi  26441  pige3ALT  26445  dfrelog  26490  logm1  26514  dvlog  26576  efopnlem2  26582  cxpexp  26593  root1id  26680  sqrt2cxp2logb9e3  26725  ang180lem2  26736  1cubrlem  26767  quart1  26782  atandm2  26803  efiasin  26814  asinsinlem  26817  asinsin  26818  asin1  26820  acos1  26821  atancj  26836  atanlogsublem  26841  efiatan2  26843  2efiatan  26844  tanatan  26845  dvatan  26861  log2cnv  26870  log2ublem2  26873  log2ublem3  26874  birthday  26880  basellem8  27014  cht1  27091  chp1  27093  ppi1i  27094  ppi2i  27095  cht2  27098  cht3  27099  bclbnd  27207  bposlem8  27218  2lgslem3c  27325  2lgslem3d  27326  noetasuplem2  27662  noetasuplem3  27663  noetasuplem4  27664  noetainflem4  27668  bday0s  27760  old0  27787  new0  27806  left1s  27827  right1s  27828  sltlpss  27840  slelss  27841  mulsproplem13  28054  mulsproplem14  28055  precsexlem1  28132  precsexlem2  28133  onsiso  28192  bdayn0sf1o  28282  ax5seglem7  28898  axlowdimlem8  28912  axlowdimlem11  28915  vtxvalsnop  29004  iedgvalsnop  29005  umgrislfupgrlem  29085  usgrexmpledg  29225  usgredgffibi  29287  vdegp1bi  29501  edginwlk  29598  uhgrwkspthlem2  29717  clwwlkvbij  30075  wlk2v2elem2  30118  frgrwopreglem3  30276  ex-dif  30385  ex-xp  30398  ex-rn  30402  ex-lcm  30420  ex-prmo  30421  ip0i  30787  ip1ilem  30788  ipdirilem  30791  ipasslem10  30801  hvnegdii  31024  hvaddcani  31027  hvsubaddi  31028  hisubcomi  31066  normlem0  31071  normlem3  31074  normlem9  31080  bcseqi  31082  norm0  31090  norm-ii-i  31099  norm3difi  31109  normpari  31116  normpar2i  31118  polid2i  31119  shs0i  31411  chj0i  31417  pjsslem  31641  ho0subi  31757  hoaddsubi  31783  hosd1i  31784  hopncani  31786  nmop0  31948  nmfn0  31949  lnopunilem1  31972  lnophmlem2  31979  opsqrlem2  32103  pjclem1  32157  atabsi  32363  dmdbr6ati  32385  inin  32478  iuninc  32522  gtiso  32657  f1od2  32677  fpwrelmapffs  32690  fzodif1  32748  nn0split01  32775  dfdec100  32788  dp20u  32831  dp3mul10  32851  dpmul1000  32852  dpexpp1  32861  dpadd2  32863  dpmul  32866  dpmul4  32867  1mhdrd  32869  cycpmrn  33098  tocyccntz  33099  cos9thpiminplylem4  33754  cos9thpiminplylem5  33755  lmat22det  33791  ordtcnvNEW  33889  ordtrest2NEW  33892  zlmtset  33932  qqhucn  33961  esumnul  34017  mbfmcst  34229  carsggect  34288  eulerpartgbij  34342  eulerpartlemn  34351  fib0  34369  fib1  34370  fib2  34372  fib3  34373  fib4  34374  fib5  34375  fib6  34376  0rrv  34421  coinflipprob  34450  ballotlem2  34459  ballotth  34508  signsvf0  34550  itgexpif  34576  hgt750lem  34621  hgt750lem2  34622  bnj1416  35008  derang0  35144  subfac0  35152  subfac1  35153  satfv1  35338  fmla  35356  fmla0  35357  fmla0xp  35358  fmla1  35362  mthmpps  35557  problem2  35641  quad3  35645  dfrdg2  35771  pprodcnveq  35859  dffv5  35900  fullfunfv  35923  ellines  36128  rankeq1o  36147  onint1  36425  bj-xpimasn  36931  bj-pr11val  36981  bj-pr21val  36989  bj-pr22val  36995  bj-nuliotaALT  37034  bj-dfmpoa  37094  bj-opabco  37164  icorempo  37327  finxpreclem4  37370  finxp2o  37375  finxp3o  37376  matunitlindf  37600  poimirlem5  37607  poimirlem22  37624  poimirlem26  37628  poimirlem30  37632  ismblfin  37643  dvtan  37652  asindmre  37685  dvasin  37686  dvacos  37687  areacirclem5  37694  heiborlem6  37798  dmcnvep  38349  dmxrncnvep  38350  xrnres4  38379  dfcoels  38409  coss0  38458  refsymrels2  38544  dfeqvrels2  38567  refrelsredund4  38611  hdmap1cbv  41784  lcm4un  41992  lcm5un  41993  lcm6un  41994  lcm7un  41995  lcm8un  41996  3lexlogpow5ineq1  42030  5bc2eq10  42118  imaopab  42207  decpmul  42264  cxpi11d  42319  tan3rdpi  42328  sin2t3rdpi  42329  cos2t3rdpi  42330  readvrec2  42337  remul02  42381  fltnltalem  42638  sum9cubes  42648  diophrw  42735  dnwech  43024  lmhmlnmsplit  43063  fgraphopab  43179  arearect  43191  areaquad  43192  oaomoencom  43293  dmnonrel  43566  imanonrel  43569  cononrel1  43570  cononrel2  43571  rclexi  43591  rtrclex  43593  dfrtrcl5  43605  sqrtcval  43617  resqrtvalex  43621  imsqrtvalex  43622  cnvtrrel  43646  dfrcl2  43650  dfrcl4  43652  iunrelexp0  43678  comptiunov2i  43682  relexpaddss  43694  brtrclfv2  43703  trclfvdecomr  43704  corcltrcl  43715  cotrclrcl  43718  fsovcnvlem  43989  neicvgnvo  44091  scottabf  44216  mnuprdlem1  44248  hashnzfz  44296  lhe4.4ex1a  44305  tgqioo2  45532  sumnnodd  45615  limsup0  45679  limsup10ex  45758  liminf10ex  45759  cosnegpi  45852  itgsin0pilem1  45935  stoweidlem13  45998  wallispilem4  46053  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem3  46061  dirkertrigeqlem1  46083  fourierdlem56  46147  fourierdlem57  46148  fourierdlem58  46149  fourierdlem62  46153  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  sqwvfoura  46213  fouriersw  46216  etransclem23  46242  etransclem36  46255  etransclem38  46257  carageniuncllem1  46506  0ome  46514  ovn02  46553  smflimlem4  46759  smflim  46762  smflim2  46791  smflimsup  46813  smfliminf  46816  fmtno0  47528  fmtno1  47529  fmtno2  47538  fmtno3  47539  fmtno4  47540  fmtno5lem4  47544  139prmALT  47584  31prm  47585  5tcu2e40  47603  3exp4mod41  47604  41prothprmlem2  47606  41prothprm  47607  nnsum3primesgbe  47780  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  tgoldbachlt  47804  isuspgrim0lem  47881  isubgr3stgrlem4  47957  isubgr3stgrlem6  47959  isubgr3stgrlem7  47960  usgrexmpl1vtx  48011  usgrexmpl1edg  48012  usgrexmpl2vtx  48016  usgrexmpl2edg  48017  gpg5gricstgr3  48078  gpgprismgr4cycllem7  48089  cznrnglem  48247  2t6m3t4e0  48336  zlmodzxzldeplem3  48491  ackval0  48669  ackval1  48670  ackval2  48671  ackval3  48672  ackval40  48682  ackval42  48685  ackval50  48687  disjdifb  48798  dftpos6  48863  tposresg  48866  tposrescnv  48867  tposres3  48869  tposid  48873  iscnrm3rlem1  48928  dfswapf2  49250  setc1onsubc  49591  sec0  49749