Theorem 3eqtrd 2266

Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)
3eqtrd.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtrd	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3		3eqtrd.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	2, 3	eqtrd 2262	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	1, 4	eqtrd 2262	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  tpeq123d  3761  diftpsn3  3812  oteq123d  3875  resiima  5092  fvun1  5708  fvmptd  5723  fmptpr  5841  caovlem2d  6210  offval  6238  ofvalg  6240  cnvf1olem  6384  nnm1  6688  updjudhcoinlf  7270  updjudhcoinrg  7271  caseinl  7281  caseinr  7282  omp1eomlem  7284  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  ltexnqq  7618  prarloclemarch  7628  ltrnqg  7630  nq02m  7675  prarloclemcalc  7712  mulnqprl  7778  mulnqpru  7779  ltexprlemloc  7817  addcanprleml  7824  recexprlem1ssu  7844  cauappcvgprlem1  7869  caucvgsrlemfv  8001  caucvgsrlemoffval  8006  recidpirqlemcalc  8067  axmulass  8083  axrnegex  8089  muladd11r  8325  addcan2  8350  addsub  8380  subsub2  8397  negsubdi2  8428  muladd  8553  mulsub  8570  cru  8772  mulreim  8774  recextlem1  8821  mulap0  8824  muleqadd  8838  divrecap  8858  div23ap  8861  div12ap  8864  divmulasscomap  8866  divcanap7  8891  conjmulap  8899  apmul1  8958  nndivtr  9175  subhalfhalf  9369  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  qapne  9863  xnegneg  10058  rexsub  10078  xnegid  10084  fseq1p1m1  10319  nn0split  10361  nnsplit  10362  fzosplitsnm1  10444  fzosplitpr  10469  fzosplitprm1  10470  ceilid  10567  flqdiv  10573  zmod10  10592  modqcyc  10611  modqaddabs  10614  mulqaddmodid  10616  modqadd2mod  10626  modqm1p1mod0  10627  modqmul12d  10630  modqadd12d  10632  modqmulmodr  10642  modqaddmulmod  10643  frecuzrdgsuc  10666  seqeq123d  10708  seqvalcd  10713  seq3f1olemqsumkj  10763  seq3f1oleml  10768  seqf1oglem2  10772  seq3id3  10776  seq3id  10777  seq3homo  10779  seq3z  10780  seqhomog  10782  exp1  10797  expnegap0  10799  expmulzap  10837  m1expeven  10838  expdivap  10842  binom3  10909  sqoddm1div8  10945  mulsubdivbinom2ap  10963  bcn1  11010  bcnp1n  11011  bcval5  11015  bcn2m1  11021  bcn2p1  11022  hashdifpr  11074  ccatlen  11162  ccatalpha  11180  ccatw2s1leng  11205  ccats1val2  11207  lswccats1  11210  swrdlend  11229  ccatswrd  11241  pfxmpt  11251  pfxfv  11255  pfxfvlsw  11266  ccatpfx  11272  pfx1  11274  pfxswrd  11277  swrdpfx  11278  pfxpfx  11279  lenrevpfxcctswrd  11283  wrdind  11293  wrd2ind  11294  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatpfx2  11308  pfxccatid  11312  cats1fvnd  11336  crim  11409  remullem  11422  remul2  11424  immul2  11431  ipcnval  11437  cjreim  11454  recvguniqlem  11545  resqrexlemover  11561  resqrexlemcalc1  11565  absid  11622  amgm2  11669  max0addsup  11770  minabs  11787  xrmaxrecl  11806  xrminadd  11826  fsumsplitf  11959  sumsnf  11960  fsump1i  11984  fsum2dlemstep  11985  fsumshftm  11996  fsummulc2  11999  modfsummodlemstep  12008  telfsumo  12017  fsumrelem  12022  hash2iun1dif1  12031  binomlem  12034  binom1dif  12038  arisum  12049  geo2sum  12065  geo2sum2  12066  cvgratz  12083  mertenslemi1  12086  clim2prod  12090  fprodeq0  12168  fprod2dlemstep  12173  fproddivap  12181  fproddivapf  12182  fprodmodd  12192  ef0lem  12211  eftlub  12241  efsep  12242  effsumlt  12243  tanval2ap  12264  efi4p  12268  resin4p  12269  recos4p  12270  efeul  12285  sinadd  12287  cosadd  12288  sinmul  12295  ef01bndlem  12307  cos12dec  12319  absef  12321  demoivreALT  12325  dvds2ln  12375  dvdseq  12399  opeo  12448  bezoutlemnewy  12557  nninfctlemfo  12601  eucalginv  12618  eucalglt  12619  eucalg  12621  lcmgcdlem  12639  lcm1  12643  divgcdcoprmex  12664  2sqpwodd  12738  zgcdsq  12763  qden1elz  12767  phiprmpw  12784  eulerthlem1  12789  eulerthlemrprm  12791  prmdiv  12797  hashgcdlem  12800  odzdvds  12808  vfermltl  12814  modprm0  12817  pythagtriplem12  12838  pcqmul  12866  pcaddlem  12902  pcadd  12903  pcadd2  12904  pcmpt  12906  pcmpt2  12907  mul4sqlem  12956  4sqlem11  12964  4sqlem17  12970  nninfdclemp1  13061  ressressg  13148  gsumsplit1r  13471  gsumprval  13472  mndinvmod  13518  mhmco  13563  gsumfzz  13568  grpinvid2  13626  grpasscan2  13637  grpinvssd  13650  grpinvadd  13651  grpsubid1  13658  grpsubadd  13661  grppncan  13664  mulg1  13706  mulgaddcomlem  13722  mulgdirlem  13730  mulgneg2  13733  mulgmodid  13738  nmzsubg  13787  qusinv  13813  qussub  13814  conjnmz  13856  ablsub2inv  13888  abladdsub4  13891  abladdsub  13892  ablpncan2  13893  ablpnpcan  13897  ablnncan  13898  invghm  13906  gsumfzconst  13918  gsumfzsnfd  13922  rngm2neg  13952  srgpcompp  13994  srgpcomppsc  13995  ringinvnzdiv  14053  ringm2neg  14058  dvr1  14142  dvrcan1  14144  dvrcan3  14145  rdivmuldivd  14148  lmodfopne  14330  sralemg  14442  gsumfzfsumlemm  14591  mplsubgfilemcl  14703  mplsubgfileminv  14704  xmetxpbl  15222  ivthinclemuopn  15352  limcimolemlt  15378  cnplimcim  15381  limccnpcntop  15389  limccnp2lem  15390  dvexp  15425  dvmptcmulcn  15435  dvply1  15479  ef2kpi  15520  sinhalfpip  15534  sinhalfpim  15535  coshalfpim  15537  ptolemy  15538  tangtx  15552  rpabscxpbnd  15654  relogbexpap  15672  rplogbcxp  15677  rpcxplogb  15678  binom4  15693  wilthlem1  15694  0sgm  15699  mpodvdsmulf1o  15704  fsumdvdsmul  15705  sgmppw  15706  0sgmppw  15707  1sgm2ppw  15709  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsval2lem  15729  lgsval4  15739  lgsval4a  15741  lgsneg  15743  lgsneg1  15744  lgsdirprm  15753  lgsdir  15754  lgsne0  15757  lgsmulsqcoprm  15765  gausslemma2dlem1a  15777  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3d1  15819  2sqlem3  15836  structiedg0val  15881  uhgr2edg  16045  usgr1e  16080  vtxdgfifival  16097  vtxdfifiun  16103  vtxdumgrfival  16104  vtxduspgrfvedgfi  16107  1loopgredg  16110  1loopgrvd2fi  16111  edginwlkd  16152  clwwlknonex2lem1  16232  peano4nninf  16544  trilpolemclim  16576  trilpolemeq1  16580  apdifflemf  16586