Theorem 3eqtri 2806

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

Syntax hints:   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  csbid  3759  un23  3995  in32  4046  dfnul2  4143  unvdif  4266  undif2  4268  undifabs  4269  difun2  4272  difdifdir  4280  dfif4  4322  dfif5  4323  tpidm23  4524  dfopif  4635  unisnOLD  4690  dfiunv2  4791  symdif0  4832  symdifid  4834  unidif0  5074  uniop  5214  xpun  5424  dfrn2  5558  dfdmf  5564  dfrnf  5612  res0  5648  resres  5661  xpssres  5684  dfima2  5724  imai  5734  ima0  5737  imaundir  5802  xpima  5832  dmresv  5849  rescnvcnv  5853  dmtpop  5867  rnsnopg  5870  resdmres  5881  dmmpt  5886  dmco  5899  co01  5906  suc0  6052  unisuc  6054  iunsuc  6060  fresaun  6327  dffv4  6445  fvssunirn  6477  f1ossf1o  6662  fpr  6689  fvsnun2OLD  6722  mpt20  7004  dmoprab  7020  rnoprab  7022  elrnmpt2res  7053  ov6g  7077  1st0  7453  2nd0  7454  dfmpt2  7550  curry1  7552  curry2  7555  fpar  7564  algrflem  7569  dftpos2  7653  tposoprab  7672  tposmpt2  7673  fvmpt2curryd  7681  wfrlem14  7713  wfrlem16  7715  dfrecs3  7754  tfrlem8  7765  seqomlem3  7832  df2o3  7859  omxpenlem  8351  dfsdom2  8373  marypha2lem2  8632  sup00  8660  epinid0  8796  scottexs  9049  scott0s  9050  infxpenc2  9180  kmlem3  9311  cdaassen  9341  ackbij1lem2  9380  compsscnv  9530  fin1a2lem12  9570  mulerpqlem  10114  1lt2nq  10132  axi2m1  10318  2p2e4  11521  numsuc  11863  numsucc  11890  decmul10add  11920  5p5e10  11922  6p4e10  11923  7p3e10  11926  xnegmnf  12357  pnfaddmnf  12377  fz12pr  12719  fz0tp  12763  fz0to3un2pr  12764  fzo13pr  12875  fzo0to2pr  12876  fzo0to3tp  12877  fzo0to42pr  12878  fzo1to4tp  12879  fldiv4p1lem1div2  12959  sq4e2t8  13285  i4  13290  crreczi  13312  fac1  13386  fac3  13389  hashkf  13441  hashinf  13444  dmhashres  13450  hashun3  13492  cshwsexa  13979  dmtrclfv  14170  abs0  14436  absi  14437  trirecip  15003  geoihalfsum  15021  esum  15217  tan0  15287  coshval  15291  ef01bndlem  15320  3dvds  15463  3dvdsdec  15464  3dvds2dec  15465  sadc0  15586  3lcm2e6woprm  15738  6lcm4e12  15739  lcmf0  15757  prmo0  16148  gcdmodi  16186  karatsuba  16196  43prm  16231  139prm  16233  631prm  16236  1259lem1  16240  1259lem2  16241  1259lem3  16242  1259lem4  16243  1259lem5  16244  2503lem1  16246  2503lem2  16247  2503lem3  16248  4001lem1  16250  4001lem2  16251  4001lem3  16252  4001lem4  16253  ndxarg  16284  setsfun  16294  setsfun0  16295  xpsc  16607  pmtrsn  18327  psgnprfval1  18330  sylow2a  18422  0frgp  18582  ablfac1eu  18863  sralem  19578  opsrtoslem2  19885  ply1plusgfvi  20012  pf1rcl  20113  restcld  21388  neitr  21396  txbasval  21822  txindis  21850  cnmpt1st  21884  cnmpt2nd  21885  ufildr  22147  restmetu  22787  cphipval2  23451  reust  23591  ehl0base  23626  ismbl  23734  mbfimaopnlem  23863  itg10  23896  itg2cnlem2  23970  itgz  23988  dvmptid  24161  cos2pi  24670  tan4thpi  24708  sincos6thpi  24709  pige3  24711  dfrelog  24753  logm1  24776  dvlog  24838  efopnlem2  24844  cxpexp  24855  root1id  24939  sqrt2cxp2logb9e3  24981  ang180lem2  24992  1cubrlem  25023  quart1  25038  atandm2  25059  efiasin  25070  asinsinlem  25073  asinsin  25074  asin1  25076  acos1  25077  atancj  25092  atanlogsublem  25097  efiatan2  25099  2efiatan  25100  tanatan  25101  dvatan  25117  log2cnv  25127  log2ublem2  25130  log2ublem3  25131  basellem8  25270  cht1  25347  chp1  25349  ppi1i  25350  ppi2i  25351  cht2  25354  cht3  25355  bclbnd  25461  bposlem8  25472  2lgslem3c  25579  2lgslem3d  25580  ax5seglem7  26288  axlowdimlem8  26302  axlowdimlem11  26305  vtxvalsnop  26393  iedgvalsnop  26394  umgrislfupgrlem  26474  usgrexmpledg  26613  usgredgffibi  26675  vdegp1bi  26889  edginwlk  26986  uhgrwkspthlem2  27110  wlksnwwlknvbijOLD  27286  clwwlkvbij  27519  clwwlkvbijOLD  27520  wlk2v2elem2  27563  frgrwopreglem3  27726  ex-dif  27859  ex-xp  27872  ex-rn  27876  ex-lcm  27894  ex-prmo  27895  ip0i  28256  ip1ilem  28257  ipdirilem  28260  ipasslem10  28270  hvnegdii  28495  hvaddcani  28498  hvsubaddi  28499  hisubcomi  28537  normlem0  28542  normlem3  28545  normlem9  28551  bcseqi  28553  norm0  28561  norm-ii-i  28570  norm3difi  28580  normpari  28587  normpar2i  28589  polid2i  28590  shs0i  28884  chj0i  28890  pjsslem  29114  ho0subi  29230  hoaddsubi  29256  hosd1i  29257  hopncani  29259  nmop0  29421  nmfn0  29422  lnopunilem1  29445  lnophmlem2  29452  opsqrlem2  29576  pjclem1  29630  atabsi  29836  dmdbr6ati  29858  inin  29918  iuninc  29945  gtiso  30048  f1od2  30069  fpwrelmapffs  30079  dfdec100  30144  dp20u  30152  dp3mul10  30172  dpmul1000  30173  dpexpp1  30182  dpadd2  30184  dpmul  30187  dpmul4  30188  1mhdrd  30190  lmat22det  30490  ordtcnvNEW  30568  ordtrest2NEW  30571  zlmtset  30611  qqhucn  30638  zrhre  30665  qqhre  30666  esumnul  30712  mbfmcst  30923  carsggect  30982  eulerpartgbij  31036  eulerpartlemn  31045  fib0  31064  fib1  31065  fib2  31067  fib3  31068  fib4  31069  fib5  31070  fib6  31071  0rrv  31116  coinflipprob  31144  ballotlem2  31153  ballotth  31202  signsvf0  31263  itgexpif  31290  hgt750lem  31335  hgt750lem2  31336  bnj1416  31710  derang0  31754  subfac0  31762  subfac1  31763  mthmpps  32082  problem2  32161  quad3  32165  dfrdg2  32293  trpred0  32328  noetalem2  32457  noetalem3  32458  pprodcnveq  32583  dffv5  32624  fullfunfv  32647  ellines  32852  rankeq1o  32871  onint1  33035  bj-xpimasn  33518  bj-pr11val  33569  bj-pr21val  33577  bj-pr22val  33583  bj-nuliotaALT  33596  bj-dfmpt2a  33648  icorempt2  33797  finxpreclem4  33829  finxp2o  33834  finxp3o  33835  matunitlindf  34038  poimirlem5  34045  poimirlem22  34062  poimirlem26  34066  poimirlem30  34070  ismblfin  34081  dvtan  34090  asindmre  34125  dvasin  34126  dvacos  34127  areacirclem5  34134  heiborlem6  34244  xrnres4  34796  dfcoels  34818  coss0  34862  refsymrels2  34944  dfeqvrels2  34965  refrelsred4  35006  hdmap1cbv  37961  sqn5ii  38158  decpmul  38160  diophrw  38292  dnwech  38587  lmhmlnmsplit  38626  fgraphopab  38757  arearect  38769  areaquad  38770  dmnonrel  38863  imanonrel  38866  cononrel1  38867  cononrel2  38868  rclexi  38889  dfrtrcl5  38903  cnvtrrel  38929  dfrcl2  38933  dfrcl4  38935  iunrelexp0  38961  comptiunov2i  38965  relexpaddss  38977  brtrclfv2  38986  trclfvdecomr  38987  corcltrcl  38998  cotrclrcl  39001  fsovcnvlem  39273  neicvgnvo  39379  hashnzfz  39485  lhe4.4ex1a  39494  disjinfi  40313  tgqioo2  40692  sumnnodd  40780  limsup0  40844  limsup10ex  40923  liminf10ex  40924  cosnegpi  41016  itgsin0pilem1  41103  stoweidlem13  41167  wallispilem4  41222  wallispi2lem1  41225  wallispi2lem2  41226  stirlinglem3  41230  dirkertrigeqlem1  41252  fourierdlem56  41316  fourierdlem57  41317  fourierdlem58  41318  fourierdlem62  41322  fourierdlem103  41363  fourierdlem104  41364  fourierdlem112  41372  sqwvfoura  41382  fouriersw  41385  etransclem23  41411  etransclem36  41424  etransclem38  41426  carageniuncllem1  41672  0ome  41680  ovn02  41719  smflimlem4  41919  smflim  41922  smflim2  41949  smflimsup  41971  smfliminf  41974  fmtno0  42483  fmtno1  42484  fmtno2  42493  fmtno3  42494  fmtno4  42495  fmtno5lem4  42499  139prmALT  42542  31prm  42543  5tcu2e40  42563  3exp4mod41  42564  41prothprmlem2  42566  41prothprm  42567  nnsum3primesgbe  42715  nnsum4primesodd  42719  nnsum4primesoddALTV  42720  nnsum4primeseven  42723  nnsum4primesevenALTV  42724  bgoldbtbndlem1  42728  tgoldbachlt  42739  cznrnglem  42978  2t6m3t4e0  43151  zlmodzxzldeplem3  43316  sec0  43619