Theorem 3eqtri 2772

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  csbid  3934  csbconstg  3940  csbie  3957  un23  4197  in32  4251  dfnul4  4354  dfnul2OLD  4357  unvdif  4498  undif2  4500  undifabs  4501  difun2  4504  difdifdir  4515  dfif4  4563  dfif5  4564  tpidm23  4782  dfopif  4894  dfiunv2  5058  symdif0  5108  symdifid  5110  unidif0  5378  uniop  5534  xpun  5773  dfrn2  5913  dfdmf  5921  dfrnf  5975  res0  6013  resres  6022  xpssres  6047  dfima2  6091  imai  6103  ima0  6106  imaundir  6182  xpima  6213  cnvrescnv  6226  dmresv  6231  rescnvcnv  6235  dmtpop  6249  rnsnopg  6252  resdmres  6263  resdifdi  6267  dmmpt  6271  dmco  6285  co01  6292  suc0  6470  iunsuc  6480  fresaun  6792  dffv4  6917  fvssunirnOLD  6954  f1ossf1o  7162  fpr  7188  mpo0  7535  dmoprab  7552  rnoprab  7554  elrnmpores  7588  ov6g  7614  1st0  8036  2nd0  8037  dfmpo  8143  curry1  8145  curry2  8148  fpar  8157  dftpos2  8284  tposoprab  8303  tposmpo  8304  fvmpocurryd  8312  frrlem14  8340  dfwrecsOLD  8354  wfrlem14OLD  8378  wfrlem16OLD  8380  dfrecs3  8428  dfrecs3OLD  8429  tfrlem8  8440  seqomlem3  8508  df2o3  8530  nlim2  8546  omxpenlem  9139  dfsdom2  9162  pwfir  9383  marypha2lem2  9505  sup00  9533  epinid0  9669  scottexs  9956  scott0s  9957  infxpenc2  10091  kmlem3  10222  ackbij1lem2  10289  compsscnv  10440  fin1a2lem12  10480  mulerpqlem  11024  1lt2nq  11042  axi2m1  11228  2p2e4  12428  numsuc  12772  numsucc  12798  decmul10add  12827  5p5e10  12829  6p4e10  12830  7p3e10  12833  xnegmnf  13272  pnfaddmnf  13292  fz12pr  13641  fz0tp  13685  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  fzo13pr  13800  fzo0to2pr  13801  fzo0to3tp  13802  fzo0to42pr  13803  fzo1to4tp  13804  fldiv4p1lem1div2  13886  sq4e2t8  14248  i4  14253  crreczi  14277  fac1  14326  fac3  14329  hashkf  14381  hashinf  14384  dmhashres  14390  hashun3  14433  cshwsexaOLD  14873  dmtrclfv  15067  abs0  15334  absi  15335  trirecip  15911  geoihalfsum  15930  esum  16128  tan0  16199  coshval  16203  ef01bndlem  16232  3dvds  16379  3dvdsdec  16380  3dvds2dec  16381  sadc0  16500  3lcm2e6woprm  16662  6lcm4e12  16663  lcmf0  16681  prmo0  17083  gcdmodi  17121  karatsuba  17131  43prm  17169  139prm  17171  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  setsfun  17218  setsfun0  17219  ndxarg  17243  pmtrsn  19561  psgnprfval1  19564  sylow2a  19661  ablfac1eu  20117  sralem  21198  sralemOLD  21199  pzriprng1ALT  21530  opsrtoslem2  22103  ply1plusgfvi  22264  pf1rcl  22374  restcld  23201  neitr  23209  txbasval  23635  txindis  23663  cnmpt1st  23697  cnmpt2nd  23698  ufildr  23960  restmetu  24604  cphipval2  25294  reust  25434  ehl0base  25469  ismbl  25580  mbfimaopnlem  25709  itg10  25742  itg2cnlem2  25817  itgz  25836  dvmptid  26015  cos2pi  26536  tan4thpi  26574  tan4thpiOLD  26575  sincos6thpi  26576  pige3ALT  26580  dfrelog  26625  logm1  26649  dvlog  26711  efopnlem2  26717  cxpexp  26728  root1id  26815  sqrt2cxp2logb9e3  26860  ang180lem2  26871  1cubrlem  26902  quart1  26917  atandm2  26938  efiasin  26949  asinsinlem  26952  asinsin  26953  asin1  26955  acos1  26956  atancj  26971  atanlogsublem  26976  efiatan2  26978  2efiatan  26979  tanatan  26980  dvatan  26996  log2cnv  27005  log2ublem2  27008  log2ublem3  27009  birthday  27015  basellem8  27149  cht1  27226  chp1  27228  ppi1i  27229  ppi2i  27230  cht2  27233  cht3  27234  bclbnd  27342  bposlem8  27353  2lgslem3c  27460  2lgslem3d  27461  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem4  27803  bday0s  27891  old0  27916  new0  27931  left1s  27951  right1s  27952  sltlpss  27963  slelss  27964  mulsproplem13  28172  mulsproplem14  28173  precsexlem1  28249  precsexlem2  28250  ax5seglem7  28968  axlowdimlem8  28982  axlowdimlem11  28985  vtxvalsnop  29076  iedgvalsnop  29077  umgrislfupgrlem  29157  usgrexmpledg  29297  usgredgffibi  29359  vdegp1bi  29573  edginwlk  29671  uhgrwkspthlem2  29790  clwwlkvbij  30145  wlk2v2elem2  30188  frgrwopreglem3  30346  ex-dif  30455  ex-xp  30468  ex-rn  30472  ex-lcm  30490  ex-prmo  30491  ip0i  30857  ip1ilem  30858  ipdirilem  30861  ipasslem10  30871  hvnegdii  31094  hvaddcani  31097  hvsubaddi  31098  hisubcomi  31136  normlem0  31141  normlem3  31144  normlem9  31150  bcseqi  31152  norm0  31160  norm-ii-i  31169  norm3difi  31179  normpari  31186  normpar2i  31188  polid2i  31189  shs0i  31481  chj0i  31487  pjsslem  31711  ho0subi  31827  hoaddsubi  31853  hosd1i  31854  hopncani  31856  nmop0  32018  nmfn0  32019  lnopunilem1  32042  lnophmlem2  32049  opsqrlem2  32173  pjclem1  32227  atabsi  32433  dmdbr6ati  32455  inin  32545  iuninc  32583  gtiso  32712  f1od2  32735  fpwrelmapffs  32748  fzodif1  32798  nn0split01  32821  dfdec100  32834  dp20u  32842  dp3mul10  32862  dpmul1000  32863  dpexpp1  32872  dpadd2  32874  dpmul  32877  dpmul4  32878  1mhdrd  32880  cycpmrn  33136  tocyccntz  33137  lmat22det  33768  ordtcnvNEW  33866  ordtrest2NEW  33869  zlmtset  33910  zlmtsetOLD  33911  qqhucn  33938  esumnul  34012  mbfmcst  34224  carsggect  34283  eulerpartgbij  34337  eulerpartlemn  34346  fib0  34364  fib1  34365  fib2  34367  fib3  34368  fib4  34369  fib5  34370  fib6  34371  0rrv  34416  coinflipprob  34444  ballotlem2  34453  ballotth  34502  signsvf0  34557  itgexpif  34583  hgt750lem  34628  hgt750lem2  34629  bnj1416  35015  derang0  35137  subfac0  35145  subfac1  35146  satfv1  35331  fmla  35349  fmla0  35350  fmla0xp  35351  fmla1  35355  mthmpps  35550  problem2  35634  quad3  35638  dfrdg2  35759  pprodcnveq  35847  dffv5  35888  fullfunfv  35911  ellines  36116  rankeq1o  36135  onint1  36415  bj-xpimasn  36921  bj-pr11val  36971  bj-pr21val  36979  bj-pr22val  36985  bj-nuliotaALT  37024  bj-dfmpoa  37084  bj-opabco  37154  icorempo  37317  finxpreclem4  37360  finxp2o  37365  finxp3o  37366  matunitlindf  37578  poimirlem5  37585  poimirlem22  37602  poimirlem26  37606  poimirlem30  37610  ismblfin  37621  dvtan  37630  asindmre  37663  dvasin  37664  dvacos  37665  areacirclem5  37672  heiborlem6  37776  xrnres4  38361  dfcoels  38386  coss0  38435  refsymrels2  38521  dfeqvrels2  38544  refrelsredund4  38588  hdmap1cbv  41759  lcm4un  41973  lcm5un  41974  lcm6un  41975  lcm7un  41976  lcm8un  41977  3lexlogpow5ineq1  42011  5bc2eq10  42099  2xp3dxp2ge1d  42198  imaopab  42224  decpmul  42277  cxpi11d  42331  tan3rdpi  42338  remul02  42381  fltnltalem  42617  sum9cubes  42627  diophrw  42715  dnwech  43005  lmhmlnmsplit  43044  fgraphopab  43164  arearect  43176  areaquad  43177  oaomoencom  43279  dmnonrel  43552  imanonrel  43555  cononrel1  43556  cononrel2  43557  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  sqrtcval  43603  resqrtvalex  43607  imsqrtvalex  43608  cnvtrrel  43632  dfrcl2  43636  dfrcl4  43638  iunrelexp0  43664  comptiunov2i  43668  relexpaddss  43680  brtrclfv2  43689  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  fsovcnvlem  43975  neicvgnvo  44077  scottabf  44209  mnuprdlem1  44241  hashnzfz  44289  lhe4.4ex1a  44298  tgqioo2  45465  sumnnodd  45551  limsup0  45615  limsup10ex  45694  liminf10ex  45695  cosnegpi  45788  itgsin0pilem1  45871  stoweidlem13  45934  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem3  45997  dirkertrigeqlem1  46019  fourierdlem56  46083  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  sqwvfoura  46149  fouriersw  46152  etransclem23  46178  etransclem36  46191  etransclem38  46193  carageniuncllem1  46442  0ome  46450  ovn02  46489  smflimlem4  46695  smflim  46698  smflim2  46727  smflimsup  46749  smfliminf  46752  fmtno0  47414  fmtno1  47415  fmtno2  47424  fmtno3  47425  fmtno4  47426  fmtno5lem4  47430  139prmALT  47470  31prm  47471  5tcu2e40  47489  3exp4mod41  47490  41prothprmlem2  47492  41prothprm  47493  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  tgoldbachlt  47690  isuspgrim0lem  47755  usgrexmpl1vtx  47838  usgrexmpl1edg  47839  usgrexmpl2vtx  47843  usgrexmpl2edg  47844  cznrnglem  47982  2t6m3t4e0  48073  zlmodzxzldeplem3  48231  ackval0  48414  ackval1  48415  ackval2  48416  ackval3  48417  ackval40  48427  ackval42  48430  ackval50  48432  disjdifb  48541  iscnrm3rlem1  48620  mndtchom  48757  sec0  48852