Theorem 3eqtri 2790

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  csbid  3864  csbconstg  3870  csbie  3886  in32  4129  un23  4175  dfnul4  4283  unvdif  4432  undif2  4434  undifabs  4437  difun2  4440  difdifdir  4450  dfif4  4501  dfif5  4502  tpidm23  4720  dfopif  4842  dfiunv2  4997  symdif0  5050  symdifv  5051  symdifid  5052  unidif0  5328  unidif0OLD  5329  uniop  5495  xpun  5732  dfrn2  5882  dfdmf  5890  dfrnf  5944  res0  5990  resres  5999  xpres  6024  dfima2  6076  imai  6090  ima0  6093  imaundir  6160  xpima  6192  cnvrescnv  6206  dmresv  6213  rescnvcnv  6224  dmtpop  6238  rnsnopg  6241  resdmres  6252  resdifdi  6256  dmmpt  6260  dmco  6275  co01  6284  relcnvtrg  6292  suc0  6466  iunsuc  6476  fresaun  6783  dffv4  6913  f1ossf1o  7161  fpr  7190  mpo0  7536  dmoprab  7554  rnoprab  7556  elrnmpores  7590  ov6g  7616  1st0  8041  2nd0  8042  f1od2  8145  dfmpo  8150  curry1  8152  curry2  8155  fpar  8164  dftpos2  8298  tposoprab  8317  tposmpo  8318  fvmpocurryd  8326  frrlem14  8355  dfrecs3  8418  tfrlem8  8430  seqomlem3  8500  df2o3  8522  nlim2  8536  omxpenlem  9135  dfsdom2  9157  pwfir  9346  marypha2lem2  9465  sup00  9494  epinid0  9636  scottabf  9976  scottexsOLD  9980  scott0bsOLD  9982  infxpenc2  10140  kmlem3  10270  ackbij1lem2  10337  compsscnv  10488  fin1a2lem12  10528  mulerpqlem  11079  1lt2nq  11097  axi2m1  11283  2p2e4  12517  numsuc  12868  numsucc  12899  decmul10add  12928  5p5e10  12930  6p4e10  12931  7p3e10  12934  xnegmnf  13380  pnfaddmnf  13400  fz12pr  13755  fz0tp  13802  fz0to3un2pr  13803  fz0to4untppr  13804  fz0to5un2tp  13805  fzo13pr  13924  fzo0to2pr  13925  fz01pr  13926  fzo0to3tp  13927  fzo0to42pr  13928  fzo1to4tp  13929  fldiv4p1lem1div2  14015  sq4e2t8  14382  i4  14388  crreczi  14413  fac1  14462  fac3  14465  hashkf  14517  hashinf  14520  dmhashres  14526  hashun3  14569  dmtrclfv  15214  abs0  15495  absi  15496  trirecip  16076  geoihalfsum  16095  esum  16290  tan0  16363  coshval  16367  ef01bndlem  16396  3dvds  16545  3dvdsdec  16546  3dvds2dec  16547  sadc0  16668  3lcm2e6woprm  16834  6lcm4e12  16835  lcmf0  16853  prmo0  17258  prmo3  17263  gcdmodi  17296  karatsuba  17305  43prm  17344  139prm  17346  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem1  17359  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  setsfun  17393  setsfun0  17394  ndxarg  17418  chnccat  18850  ex-chn2  18862  pmtrsn  19784  psgnprfval1  19787  sylow2a  19884  ablfac1eu  20340  sralem  21502  pzriprng1ALT  21857  opsrtoslem2  22420  ply1plusgfvi  22614  pf1rcl  22722  matunitlindf  23051  restcld  23545  neitr  23553  txbasval  23980  txindis  24008  cnmpt1st  24042  cnmpt2nd  24043  ufildr  24305  restmetu  24944  cphipval2  25617  reust  25757  ehl0base  25792  ismbl  25902  mbfimaopnlem  26031  itg10  26064  itg2cnlem2  26138  itgz  26156  dvmptid  26332  cos2pi  26862  tan4thpi  26900  sincos6thpi  26901  pige3ALT  26905  dfrelog  26950  logm1  26974  dvlog  27036  efopnlem2  27042  cxpexp  27053  root1id  27139  sqrt2cxp2logb9e3  27184  ang180lem2  27195  1cubrlem  27226  quart1  27241  atandm2  27262  efiasin  27273  asinsinlem  27276  asinsin  27277  asin1  27279  acos1  27280  atancj  27295  atanlogsublem  27300  efiatan2  27302  2efiatan  27303  tanatan  27304  dvatan  27320  log2cnv  27329  log2ublem2  27332  log2ublem3  27333  birthday  27339  cht1  27549  chp1  27551  ppi1i  27552  ppi2i  27553  cht2  27556  cht3  27557  bclbnd  27664  bposlem8  27675  2lgslem3c  27782  2lgslem3d  27783  noetasuplem2  28148  noetasuplem3  28149  noetasuplem4  28150  noetainflem4  28154  bday0  28254  old0  28282  new0  28307  left1s  28338  right1s  28339  ltslpss  28351  leslss  28352  mulsproplem13  28571  mulsproplem14  28572  precsexlem1  28650  precsexlem2  28651  oniso  28714  bdayn0sf1o  28813  ax5seglem7  29570  axlowdimlem8  29584  axlowdimlem11  29587  vtxvalsnop  29676  iedgvalsnop  29677  umgrislfupgrlem  29757  usgrexmpledg  29900  usgredgffibi  29962  vdegp1bi  30175  edginwlk  30272  clwwlkvbij  30761  wlk2v2elem2  30814  frgrwopreglem3  30972  ex-dif  31081  ex-xp  31094  ex-rn  31098  ex-lcm  31116  ex-prmo  31117  ip0i  31484  ip1ilem  31485  ipdirilem  31488  ipasslem10  31498  hvnegdii  31721  hvaddcani  31724  hvsubaddi  31725  hisubcomi  31763  normlem0  31768  normlem3  31771  normlem9  31777  bcseqi  31779  norm0  31787  norm-ii-i  31796  norm3difi  31806  normpari  31813  normpar2i  31815  polid2i  31816  shs0i  32108  chj0i  32114  pjsslem  32338  ho0subi  32454  hoaddsubi  32480  hosd1i  32481  hopncani  32483  nmop0  32645  nmfn0  32646  lnopunilem1  32669  lnophmlem2  32676  opsqrlem2  32800  pjclem1  32854  atabsi  33060  dmdbr6ati  33082  inin  33211  iuninc  33253  gtiso  33391  fpwrelmapffs  33422  fzodif1  33480  nn0split01  33505  dfdec100  33517  dp20u  33540  dp3mul10  33560  dpmul1000  33561  dpexpp1  33570  dpadd2  33572  dpmul  33575  dpmul4  33576  1mhdrd  33578  cycpmrn  33803  tocyccntz  33804  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  lmat22det  34565  ordtcnvNEW  34663  ordtrest2NEW  34666  zlmtset  34706  qqhucn  34735  esumnul  34791  mbfmcst  35002  carsggect  35061  eulerpartgbij  35115  eulerpartlemn  35124  fib0  35142  fib1  35143  fib2  35145  fib3  35146  fib4  35147  fib5  35148  fib6  35149  0rrv  35194  coinflipprob  35223  ballotlem2  35232  ballotth  35281  signsvf0  35320  itgexpif  35346  hgt750lem  35391  hgt750lem2  35392  bnj1416  35780  mpofvd  35838  r11  35850  r12  35851  derang0  36142  subfac0  36150  subfac1  36151  satfv1  36336  fmla  36354  fmla0  36355  fmla0xp  36356  fmla1  36360  mthmpps  36555  problem2  36639  quad3  36643  dfrdg2  36772  pprodcnveq  36860  dffv5  36901  dfsuccf2  36920  fullfunfv  36926  ellines  37132  rankeq1o  37147  onint1  37452  bj-xpimasn  38083  bj-pr11val  38133  bj-pr21val  38141  bj-pr22val  38147  bj-nuliotaALT  38243  bj-dfmpoa  38310  bj-opabco  38377  icorempo  38542  finxpreclem4  38585  finxp2o  38590  finxp3o  38591  poimirlem5  38811  poimirlem22  38828  poimirlem26  38832  poimirlem30  38836  ismblfin  38847  dvtan  38856  asindmre  38889  dvasin  38890  dvacos  38891  areacirclem5  38898  heiborlem6  39016  dmcnvep  39586  dmxrncnvep  39587  dmcnvepres  39588  dmxrnuncnvepres  39590  xrnres4  39626  dfadjliftmap2  39655  blockadjliftmap  39656  dfblockliftmap2  39659  dfsucmap3  39661  dfsuccl2  39668  dfcoels  39718  coss0  39767  refsymrels2  39847  dfeqvrels2  39870  refrelsredund4  39914  hdmap1cbv  43125  lcm4un  43332  lcm5un  43333  lcm6un  43334  lcm7un  43335  lcm8un  43336  3lexlogpow5ineq1  43370  5bc2eq10  43458  imaopab  43552  decpmul  43611  cxpi11d  43660  tan3rdpi  43669  sin2t3rdpi  43670  cos2t3rdpi  43671  readvrec2  43678  remul02  43722  fltnltalem  43939  sum9cubes  43949  diophrw  44036  dnwech  44321  lmhmlnmsplit  44355  fgraphopab  44466  arearect  44478  areaquad  44479  oaomoencom  44580  dmnonrel  44851  imanonrel  44854  cononrel1  44855  cononrel2  44856  rclexi  44876  rtrclex  44878  dfrtrcl5  44890  sqrtcval  44902  resqrtvalex  44906  imsqrtvalex  44907  cnvtrrel  44931  dfrcl2  44935  dfrcl4  44937  iunrelexp0  44963  comptiunov2i  44967  relexpaddss  44979  brtrclfv2  44988  trclfvdecomr  44989  corcltrcl  45000  cotrclrcl  45003  fsovcnvlem  45274  neicvgnvo  45376  k0004val0  45415  mnuprdlem1  45517  hashnzfz  45565  lhe4.4ex1a  45574  tgqioo2  46832  sumnnodd  46915  limsup0  46977  limsup10ex  47056  liminf10ex  47057  cosnegpi  47150  itgsin0pilem1  47233  stoweidlem13  47296  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem3  47359  dirkertrigeqlem1  47381  fourierdlem56  47445  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fourierdlem103  47492  fourierdlem104  47493  fourierdlem112  47501  sqwvfoura  47511  fouriersw  47514  etransclem23  47540  etransclem36  47553  etransclem38  47555  carageniuncllem1  47804  0ome  47812  ovn02  47851  smflimlem4  48057  smflim  48060  smflim2  48089  smflimsup  48111  smfliminf  48114  numtowerdt  48189  cos5t  48198  goldpolyfactor  48200  goldratmolem2  48206  goldratval  48209  cjnpoly  48212  fmtno0  48898  fmtno1  48899  fmtno2  48908  fmtno3  48909  fmtno4  48910  fmtno5lem4  48914  139prmALT  48954  31prm  48955  5tcu2e40  48973  3exp4mod41  48974  41prothprmlem2  48976  41prothprm  48977  ppivalnn4  48985  nnsum3primesgbe  49163  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbtbndlem1  49176  tgoldbachlt  49187  isuspgrim0lem  49264  isubgr3stgrlem4  49340  isubgr3stgrlem6  49342  isubgr3stgrlem7  49343  usgrexmpl1vtx  49394  usgrexmpl1edg  49395  usgrexmpl2vtx  49399  usgrexmpl2edg  49400  gpg5gricstgr3  49461  gpgprismgr4cycllem7  49472  cznrnglem  49629  bru2  49751  bru3val  49753  bru3cj  49754  bru3sq  49755  bru3eq  49756  2t6m3t4e0  49791  zlmodzxzldeplem3  49945  ackval0  50123  ackval1  50124  ackval2  50125  ackval3  50126  ackval40  50136  ackval42  50139  ackval50  50141  disjdifb  50251  dftpos6  50319  tposresg  50322  tposrescnv  50323  tposres3  50325  tposid  50329  iscnrm3rlem1  50385  dfswapf2  50714  setc1onsubc  51071  parswapprop  51108  par2hom  51110  fuconuniqlem  51112  fuconuniqvalslem  51114  sinh0  51241  cosh0  51245  tanh0  51251  sec0  51281  dvcsc  51285  dvcot  51286