Theorem 3eqtri 2764

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 2760	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2760	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  csbid  3851  csbconstg  3857  csbie  3873  un23  4115  in32  4171  dfnul4  4276  unvdif  4416  undif2  4418  undifabs  4419  difun2  4422  difdifdir  4432  dfif4  4483  dfif5  4484  tpidm23  4702  dfopif  4814  dfiunv2  4977  symdif0  5028  symdifv  5029  symdifid  5030  unidif0  5297  uniop  5463  xpun  5698  dfrn2  5837  dfdmf  5845  dfrnf  5899  res0  5942  resres  5951  xpssres  5977  dfima2  6021  imai  6033  ima0  6036  imaundir  6108  xpima  6140  cnvrescnv  6153  dmresv  6158  rescnvcnv  6162  dmtpop  6176  rnsnopg  6179  resdmres  6190  resdifdi  6194  dmmpt  6198  dmco  6213  co01  6220  suc0  6394  iunsuc  6404  fresaun  6705  dffv4  6831  f1ossf1o  7075  fpr  7101  mpo0  7445  dmoprab  7463  rnoprab  7465  elrnmpores  7498  ov6g  7524  1st0  7941  2nd0  7942  dfmpo  8045  curry1  8047  curry2  8050  fpar  8059  dftpos2  8186  tposoprab  8205  tposmpo  8206  fvmpocurryd  8214  frrlem14  8242  dfrecs3  8305  tfrlem8  8316  seqomlem3  8384  df2o3  8406  nlim2  8418  omxpenlem  9009  dfsdom2  9031  pwfir  9220  marypha2lem2  9342  sup00  9371  epinid0  9511  scottexs  9802  scott0s  9803  infxpenc2  9935  kmlem3  10066  ackbij1lem2  10133  compsscnv  10284  fin1a2lem12  10324  mulerpqlem  10869  1lt2nq  10887  axi2m1  11073  2p2e4  12302  numsuc  12649  numsucc  12675  decmul10add  12704  5p5e10  12706  6p4e10  12707  7p3e10  12710  xnegmnf  13153  pnfaddmnf  13173  fz12pr  13526  fz0tp  13573  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  fzo13pr  13695  fzo0to2pr  13696  fz01pr  13697  fzo0to3tp  13698  fzo0to42pr  13699  fzo1to4tp  13700  fldiv4p1lem1div2  13785  sq4e2t8  14152  i4  14157  crreczi  14181  fac1  14230  fac3  14233  hashkf  14285  hashinf  14288  dmhashres  14294  hashun3  14337  dmtrclfv  14971  abs0  15238  absi  15239  trirecip  15819  geoihalfsum  15838  esum  16036  tan0  16109  coshval  16113  ef01bndlem  16142  3dvds  16291  3dvdsdec  16292  3dvds2dec  16293  sadc0  16414  3lcm2e6woprm  16575  6lcm4e12  16576  lcmf0  16594  prmo0  16998  gcdmodi  17036  karatsuba  17045  43prm  17083  139prm  17085  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  setsfun  17132  setsfun0  17133  ndxarg  17157  chnccat  18583  ex-chn2  18595  pmtrsn  19485  psgnprfval1  19488  sylow2a  19585  ablfac1eu  20041  sralem  21163  pzriprng1ALT  21486  opsrtoslem2  22044  ply1plusgfvi  22215  pf1rcl  22324  restcld  23147  neitr  23155  txbasval  23581  txindis  23609  cnmpt1st  23643  cnmpt2nd  23644  ufildr  23906  restmetu  24545  cphipval2  25218  reust  25358  ehl0base  25393  ismbl  25503  mbfimaopnlem  25632  itg10  25665  itg2cnlem2  25739  itgz  25758  dvmptid  25934  cos2pi  26453  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  pige3ALT  26497  dfrelog  26542  logm1  26566  dvlog  26628  efopnlem2  26634  cxpexp  26645  root1id  26731  sqrt2cxp2logb9e3  26776  ang180lem2  26787  1cubrlem  26818  quart1  26833  atandm2  26854  efiasin  26865  asinsinlem  26868  asinsin  26869  asin1  26871  acos1  26872  atancj  26887  atanlogsublem  26892  efiatan2  26894  2efiatan  26895  tanatan  26896  dvatan  26912  log2cnv  26921  log2ublem2  26924  log2ublem3  26925  birthday  26931  basellem8  27065  cht1  27142  chp1  27144  ppi1i  27145  ppi2i  27146  cht2  27149  cht3  27150  bclbnd  27257  bposlem8  27268  2lgslem3c  27375  2lgslem3d  27376  noetasuplem2  27712  noetasuplem3  27713  noetasuplem4  27714  noetainflem4  27718  bday0  27817  old0  27845  new0  27870  left1s  27901  right1s  27902  ltslpss  27914  leslss  27915  mulsproplem13  28134  mulsproplem14  28135  precsexlem1  28213  precsexlem2  28214  oniso  28277  bdayn0sf1o  28376  ax5seglem7  29018  axlowdimlem8  29032  axlowdimlem11  29035  vtxvalsnop  29124  iedgvalsnop  29125  umgrislfupgrlem  29205  usgrexmpledg  29345  usgredgffibi  29407  vdegp1bi  29621  edginwlk  29718  uhgrwkspthlem2  29837  clwwlkvbij  30198  wlk2v2elem2  30241  frgrwopreglem3  30399  ex-dif  30508  ex-xp  30521  ex-rn  30525  ex-lcm  30543  ex-prmo  30544  ip0i  30911  ip1ilem  30912  ipdirilem  30915  ipasslem10  30925  hvnegdii  31148  hvaddcani  31151  hvsubaddi  31152  hisubcomi  31190  normlem0  31195  normlem3  31198  normlem9  31204  bcseqi  31206  norm0  31214  norm-ii-i  31223  norm3difi  31233  normpari  31240  normpar2i  31242  polid2i  31243  shs0i  31535  chj0i  31541  pjsslem  31765  ho0subi  31881  hoaddsubi  31907  hosd1i  31908  hopncani  31910  nmop0  32072  nmfn0  32073  lnopunilem1  32096  lnophmlem2  32103  opsqrlem2  32227  pjclem1  32281  atabsi  32487  dmdbr6ati  32509  inin  32601  iuninc  32645  gtiso  32789  f1od2  32807  fpwrelmapffs  32822  fzodif1  32880  nn0split01  32906  dfdec100  32918  dp20u  32952  dp3mul10  32972  dpmul1000  32973  dpexpp1  32982  dpadd2  32984  dpmul  32987  dpmul4  32988  1mhdrd  32990  cycpmrn  33219  tocyccntz  33220  cos9thpiminplylem4  33945  cos9thpiminplylem5  33946  lmat22det  33982  ordtcnvNEW  34080  ordtrest2NEW  34083  zlmtset  34123  qqhucn  34152  esumnul  34208  mbfmcst  34419  carsggect  34478  eulerpartgbij  34532  eulerpartlemn  34541  fib0  34559  fib1  34560  fib2  34562  fib3  34563  fib4  34564  fib5  34565  fib6  34566  0rrv  34611  coinflipprob  34640  ballotlem2  34649  ballotth  34698  signsvf0  34740  itgexpif  34766  hgt750lem  34811  hgt750lem2  34812  bnj1416  35197  r11  35253  r12  35254  derang0  35367  subfac0  35375  subfac1  35376  satfv1  35561  fmla  35579  fmla0  35580  fmla0xp  35581  fmla1  35585  mthmpps  35780  problem2  35864  quad3  35868  dfrdg2  35991  pprodcnveq  36079  dffv5  36120  dfsuccf2  36139  fullfunfv  36145  ellines  36350  rankeq1o  36369  onint1  36647  bj-xpimasn  37278  bj-pr11val  37328  bj-pr21val  37336  bj-pr22val  37342  bj-nuliotaALT  37381  bj-dfmpoa  37446  bj-opabco  37518  icorempo  37681  finxpreclem4  37724  finxp2o  37729  finxp3o  37730  matunitlindf  37953  poimirlem5  37960  poimirlem22  37977  poimirlem26  37981  poimirlem30  37985  ismblfin  37996  dvtan  38005  asindmre  38038  dvasin  38039  dvacos  38040  areacirclem5  38047  heiborlem6  38151  dmcnvep  38723  dmxrncnvep  38724  dmcnvepres  38725  dmxrnuncnvepres  38727  xrnres4  38763  dfadjliftmap2  38792  blockadjliftmap  38793  dfblockliftmap2  38796  dfsucmap3  38798  dfsuccl2  38805  dfcoels  38855  coss0  38904  refsymrels2  38984  dfeqvrels2  39007  refrelsredund4  39051  hdmap1cbv  42262  lcm4un  42469  lcm5un  42470  lcm6un  42471  lcm7un  42472  lcm8un  42473  3lexlogpow5ineq1  42507  5bc2eq10  42595  imaopab  42686  decpmul  42734  cxpi11d  42789  tan3rdpi  42798  sin2t3rdpi  42799  cos2t3rdpi  42800  readvrec2  42807  remul02  42851  fltnltalem  43109  sum9cubes  43119  diophrw  43205  dnwech  43494  lmhmlnmsplit  43533  fgraphopab  43649  arearect  43661  areaquad  43662  oaomoencom  43763  dmnonrel  44035  imanonrel  44038  cononrel1  44039  cononrel2  44040  rclexi  44060  rtrclex  44062  dfrtrcl5  44074  sqrtcval  44086  resqrtvalex  44090  imsqrtvalex  44091  cnvtrrel  44115  dfrcl2  44119  dfrcl4  44121  iunrelexp0  44147  comptiunov2i  44151  relexpaddss  44163  brtrclfv2  44172  trclfvdecomr  44173  corcltrcl  44184  cotrclrcl  44187  fsovcnvlem  44458  neicvgnvo  44560  scottabf  44685  mnuprdlem1  44717  hashnzfz  44765  lhe4.4ex1a  44774  tgqioo2  45995  sumnnodd  46078  limsup0  46140  limsup10ex  46219  liminf10ex  46220  cosnegpi  46313  itgsin0pilem1  46396  stoweidlem13  46459  wallispilem4  46514  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem3  46522  dirkertrigeqlem1  46544  fourierdlem56  46608  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  sqwvfoura  46674  fouriersw  46677  etransclem23  46703  etransclem36  46716  etransclem38  46718  carageniuncllem1  46967  0ome  46975  ovn02  47014  smflimlem4  47220  smflim  47223  smflim2  47252  smflimsup  47274  smfliminf  47277  fmtno0  48015  fmtno1  48016  fmtno2  48025  fmtno3  48026  fmtno4  48027  fmtno5lem4  48031  139prmALT  48071  31prm  48072  5tcu2e40  48090  3exp4mod41  48091  41prothprmlem2  48093  41prothprm  48094  ppivalnn4  48102  nnsum3primesgbe  48280  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  tgoldbachlt  48304  isuspgrim0lem  48381  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  isubgr3stgrlem7  48460  usgrexmpl1vtx  48511  usgrexmpl1edg  48512  usgrexmpl2vtx  48516  usgrexmpl2edg  48517  gpg5gricstgr3  48578  gpgprismgr4cycllem7  48589  cznrnglem  48747  2t6m3t4e0  48836  zlmodzxzldeplem3  48990  ackval0  49168  ackval1  49169  ackval2  49170  ackval3  49171  ackval40  49181  ackval42  49184  ackval50  49186  disjdifb  49297  dftpos6  49362  tposresg  49365  tposrescnv  49366  tposres3  49368  tposid  49372  iscnrm3rlem1  49427  dfswapf2  49748  setc1onsubc  50089  sec0  50247