Theorem 3eqtri 2636

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  csbid  3507  un23  3734  in32  3787  unvdif  3994  undif2  3996  undifabs  3997  difun2  4000  difdifdir  4008  dfif4  4051  dfif5  4052  tpidm23  4236  dfopif  4337  unisn  4387  dfiunv2  4492  symdif0  4533  symdifid  4535  unidif0  4764  uniop  4902  xpun  5099  dfrn2  5233  dfdmf  5239  dfrnf  5285  res0  5321  resres  5329  xpssres  5354  dfima2  5387  imai  5397  ima0  5400  imaundir  5465  xpima  5495  dmresv  5511  rescnvcnv  5515  dmtpop  5529  rnsnopg  5532  resdmres  5543  dmmpt  5547  dmco  5560  co01  5567  suc0  5716  unisuc  5718  iunsuc  5724  fresaun  5988  dffv4  6100  fvssunirn  6127  fpr  6326  fvsnun2  6354  mpt20  6623  dmoprab  6639  rnoprab  6641  elrnmpt2res  6672  ov6g  6696  1st0  7065  2nd0  7066  dfmpt2  7154  curry1  7156  curry2  7159  fpar  7168  algrflem  7173  dftpos2  7256  tposoprab  7275  tposmpt2  7276  fvmpt2curryd  7284  wfrlem14  7315  wfrlem16  7317  dfrecs3  7356  tfrlem8  7367  seqomlem3  7434  df2o3  7460  omxpenlem  7946  dfsdom2  7968  marypha2lem2  8225  scottexs  8633  scott0s  8634  infxpenc2  8728  kmlem3  8857  cdaassen  8887  ackbij1lem2  8926  compsscnv  9076  fin1a2lem12  9116  mulerpqlem  9656  1lt2nq  9674  axi2m1  9859  2p2e4  11021  numsuc  11387  numsucc  11425  decmul10add  11469  decmul10addOLD  11470  5p5e10  11472  6p4e10  11474  7p3e10  11479  xnegmnf  11915  pnfaddmnf  11935  fz0tp  12309  fz0to3un2pr  12310  fzo13pr  12419  fzo0to2pr  12420  fzo0to3tp  12421  fzo0to42pr  12422  fzo1to4tp  12423  sq4e2t8  12824  i4  12829  crreczi  12851  fac1  12926  fac3  12929  hashkf  12981  hashinf  12984  dmhashres  12991  hashun3  13034  cshwsexa  13421  dmtrclfv  13607  abs0  13873  absi  13874  trirecip  14434  geoihalfsum  14453  esum  14650  tan0  14720  coshval  14724  ef01bndlem  14753  3dvds  14890  3dvdsOLD  14891  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  sadc0  15014  3lcm2e6woprm  15166  6lcm4e12  15167  lcmf0  15185  prmo0  15578  gcdmodi  15616  karatsuba  15630  karatsubaOLD  15631  43prm  15667  139prm  15669  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  2503lem1  15682  2503lem2  15683  2503lem3  15684  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  ndxarg  15715  setsfun  15725  setsfun0  15726  xpsc  16040  pmtrsn  17762  psgnprfval1  17765  sylow2a  17857  0frgp  18015  ablfac1eu  18295  sralem  18998  opsrtoslem2  19306  ply1plusgfvi  19433  pf1rcl  19534  restcld  20786  neitr  20794  txbasval  21219  txindis  21247  cnmpt1st  21281  cnmpt2nd  21282  ufildr  21545  restmetu  22185  cphipval2  22848  reust  22977  ismbl  23101  mbfimaopnlem  23228  itg10  23261  itg2cnlem2  23335  itgz  23353  dvmptid  23526  cos2pi  24032  tan4thpi  24070  sincos6thpi  24071  pige3  24073  dfrelog  24116  logm1  24139  dvlog  24197  efopnlem2  24203  cxpexp  24214  root1id  24295  ang180lem2  24340  1cubrlem  24368  quart1  24383  atandm2  24404  efiasin  24415  asinsinlem  24418  asinsin  24419  asin1  24421  acos1  24422  atancj  24437  atanlogsublem  24442  efiatan2  24444  2efiatan  24445  tanatan  24446  dvatan  24462  log2cnv  24471  log2ublem2  24474  log2ublem3  24475  basellem8  24614  cht1  24691  chp1  24693  ppi1i  24694  ppi2i  24695  cht2  24698  cht3  24699  bclbnd  24805  bposlem8  24816  2lgslem3c  24923  2lgslem3d  24924  ax5seglem7  25615  axlowdimlem8  25629  axlowdimlem11  25632  umgrislfupgrlem  25788  wlkntrllem2  26090  constr1trl  26118  constr2spthlem1  26124  constr3trllem3  26180  constr3pthlem1  26183  constr3pthlem3  26185  wlknwwlknvbij  26268  clwwlkvbij  26329  vdegp1ai  26511  ex-dif  26672  ex-xp  26685  ex-rn  26689  ex-lcm  26707  ex-prmo  26708  ip0i  27064  ip1ilem  27065  ipdirilem  27068  ipasslem10  27078  hvnegdii  27303  hvaddcani  27306  hvsubaddi  27307  hisubcomi  27345  normlem0  27350  normlem3  27353  normlem9  27359  bcseqi  27361  norm0  27369  norm-ii-i  27378  norm3difi  27388  normpari  27395  normpar2i  27397  polid2i  27398  shs0i  27692  chj0i  27698  pjsslem  27922  ho0subi  28038  hoaddsubi  28064  hosd1i  28065  hopncani  28067  nmop0  28229  nmfn0  28230  lnopunilem1  28253  lnophmlem2  28260  opsqrlem2  28384  pjclem1  28438  atabsi  28644  dmdbr6ati  28666  inin  28737  iuninc  28761  gtiso  28861  fpwrelmapffs  28897  lmat22det  29216  ordtcnvNEW  29294  ordtrest2NEW  29297  zlmtset  29337  qqhucn  29364  zrhre  29391  qqhre  29392  esumnul  29437  mbfmcst  29648  carsggect  29707  eulerpartgbij  29761  eulerpartlemn  29770  fib0  29788  fib1  29789  fib2  29791  fib3  29792  fib4  29793  fib5  29794  fib6  29795  0rrv  29840  coinflipprob  29868  ballotlem2  29877  ballotth  29926  signsvf0  29983  bnj1416  30361  derang0  30405  subfac0  30413  subfac1  30414  mthmpps  30733  problem2  30813  problem2OLD  30814  quad3  30818  dfrdg2  30945  trpred0  30980  pprodcnveq  31160  dffv5  31201  fullfunfv  31224  ellines  31429  rankeq1o  31448  onint1  31618  bj-xpimasn  32135  bj-pr11val  32186  bj-pr21val  32194  bj-pr22val  32200  bj-nuliotaALT  32211  bj-dfmpt2a  32252  icorempt2  32375  finxpreclem4  32407  finxp2o  32412  finxp3o  32413  matunitlindf  32577  poimirlem5  32584  poimirlem22  32601  poimirlem26  32605  poimirlem30  32609  ismblfin  32620  dvtan  32630  asindmre  32665  dvasin  32666  dvacos  32667  areacirclem5  32674  heiborlem6  32785  hdmap1cbv  36110  diophrw  36340  dnwech  36636  lmhmlnmsplit  36675  fgraphopab  36807  arearect  36820  areaquad  36821  dmnonrel  36915  imanonrel  36918  cononrel1  36919  cononrel2  36920  rclexi  36941  dfrtrcl5  36955  cnvtrrel  36981  dfrcl2  36985  dfrcl4  36987  iunrelexp0  37013  comptiunov2i  37017  relexpaddss  37029  brtrclfv2  37038  trclfvdecomr  37039  corcltrcl  37050  cotrclrcl  37053  fsovcnvlem  37327  neicvgnvo  37433  hashnzfz  37541  lhe4.4ex1a  37550  disjinfi  38375  tgqioo2  38621  sumnnodd  38697  cosnegpi  38750  itgsin0pilem1  38841  stoweidlem13  38906  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem3  38969  dirkertrigeqlem1  38991  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  sqwvfoura  39121  fouriersw  39124  etransclem23  39150  etransclem36  39163  etransclem38  39165  carageniuncllem1  39411  0ome  39419  ovn02  39458  smflimlem4  39660  smflim  39663  fmtno0  39990  fmtno1  39991  fmtno2  40000  fmtno3  40001  fmtno4  40002  fmtno5lem4  40006  139prmALT  40049  31prm  40050  5tcu2e40  40070  3exp4mod41  40071  41prothprmlem2  40073  41prothprm  40074  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  tgoldbachlt  40230  tgoldbachltOLD  40237  usgrexmpledg  40486  vdegp1bi-av  40753  uhgr1wlkspthlem2  40960  wlksnwwlknvbij  41114  clwwlksvbij  41229  1wlk2v2elem2  41323  cznrnglem  41745  2t6m3t4e0  41919  zlmodzxzldeplem3  42085  sec0  42300