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  3758  diftpsn3  3809  oteq123d  3872  resiima  5086  fvun1  5702  fvmptd  5717  fmptpr  5835  caovlem2d  6204  offval  6232  ofvalg  6234  cnvf1olem  6376  nnm1  6679  updjudhcoinlf  7255  updjudhcoinrg  7256  caseinl  7266  caseinr  7267  omp1eomlem  7269  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  ltexnqq  7603  prarloclemarch  7613  ltrnqg  7615  nq02m  7660  prarloclemcalc  7697  mulnqprl  7763  mulnqpru  7764  ltexprlemloc  7802  addcanprleml  7809  recexprlem1ssu  7829  cauappcvgprlem1  7854  caucvgsrlemfv  7986  caucvgsrlemoffval  7991  recidpirqlemcalc  8052  axmulass  8068  axrnegex  8074  muladd11r  8310  addcan2  8335  addsub  8365  subsub2  8382  negsubdi2  8413  muladd  8538  mulsub  8555  cru  8757  mulreim  8759  recextlem1  8806  mulap0  8809  muleqadd  8823  divrecap  8843  div23ap  8846  div12ap  8849  divmulasscomap  8851  divcanap7  8876  conjmulap  8884  apmul1  8943  nndivtr  9160  subhalfhalf  9354  xp1d2m1eqxm1d2  9372  div4p1lem1div2  9373  qapne  9842  xnegneg  10037  rexsub  10057  xnegid  10063  fseq1p1m1  10298  nn0split  10340  nnsplit  10341  fzosplitsnm1  10423  fzosplitprm1  10448  ceilid  10545  flqdiv  10551  zmod10  10570  modqcyc  10589  modqaddabs  10592  mulqaddmodid  10594  modqadd2mod  10604  modqm1p1mod0  10605  modqmul12d  10608  modqadd12d  10610  modqmulmodr  10620  modqaddmulmod  10621  frecuzrdgsuc  10644  seqeq123d  10686  seqvalcd  10691  seq3f1olemqsumkj  10741  seq3f1oleml  10746  seqf1oglem2  10750  seq3id3  10754  seq3id  10755  seq3homo  10757  seq3z  10758  seqhomog  10760  exp1  10775  expnegap0  10777  expmulzap  10815  m1expeven  10816  expdivap  10820  binom3  10887  sqoddm1div8  10923  mulsubdivbinom2ap  10941  bcn1  10988  bcnp1n  10989  bcval5  10993  bcn2m1  10999  bcn2p1  11000  hashdifpr  11050  ccatlen  11138  ccats1val2  11179  lswccats1  11182  swrdlend  11198  ccatswrd  11210  pfxmpt  11220  pfxfv  11224  pfxfvlsw  11235  ccatpfx  11241  pfx1  11243  pfxswrd  11246  swrdpfx  11247  pfxpfx  11248  lenrevpfxcctswrd  11252  wrdind  11262  wrd2ind  11263  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatpfx2  11277  pfxccatid  11281  cats1fvnd  11305  crim  11377  remullem  11390  remul2  11392  immul2  11399  ipcnval  11405  cjreim  11422  recvguniqlem  11513  resqrexlemover  11529  resqrexlemcalc1  11533  absid  11590  amgm2  11637  max0addsup  11738  minabs  11755  xrmaxrecl  11774  xrminadd  11794  fsumsplitf  11927  sumsnf  11928  fsump1i  11952  fsum2dlemstep  11953  fsumshftm  11964  fsummulc2  11967  modfsummodlemstep  11976  telfsumo  11985  fsumrelem  11990  hash2iun1dif1  11999  binomlem  12002  binom1dif  12006  arisum  12017  geo2sum  12033  geo2sum2  12034  cvgratz  12051  mertenslemi1  12054  clim2prod  12058  fprodeq0  12136  fprod2dlemstep  12141  fproddivap  12149  fproddivapf  12150  fprodmodd  12160  ef0lem  12179  eftlub  12209  efsep  12210  effsumlt  12211  tanval2ap  12232  efi4p  12236  resin4p  12237  recos4p  12238  efeul  12253  sinadd  12255  cosadd  12256  sinmul  12263  ef01bndlem  12275  cos12dec  12287  absef  12289  demoivreALT  12293  dvds2ln  12343  dvdseq  12367  opeo  12416  bezoutlemnewy  12525  nninfctlemfo  12569  eucalginv  12586  eucalglt  12587  eucalg  12589  lcmgcdlem  12607  lcm1  12611  divgcdcoprmex  12632  2sqpwodd  12706  zgcdsq  12731  qden1elz  12735  phiprmpw  12752  eulerthlem1  12757  eulerthlemrprm  12759  prmdiv  12765  hashgcdlem  12768  odzdvds  12776  vfermltl  12782  modprm0  12785  pythagtriplem12  12806  pcqmul  12834  pcaddlem  12870  pcadd  12871  pcadd2  12872  pcmpt  12874  pcmpt2  12875  mul4sqlem  12924  4sqlem11  12932  4sqlem17  12938  nninfdclemp1  13029  ressressg  13116  gsumsplit1r  13439  gsumprval  13440  mndinvmod  13486  mhmco  13531  gsumfzz  13536  grpinvid2  13594  grpasscan2  13605  grpinvssd  13618  grpinvadd  13619  grpsubid1  13626  grpsubadd  13629  grppncan  13632  mulg1  13674  mulgaddcomlem  13690  mulgdirlem  13698  mulgneg2  13701  mulgmodid  13706  nmzsubg  13755  qusinv  13781  qussub  13782  conjnmz  13824  ablsub2inv  13856  abladdsub4  13859  abladdsub  13860  ablpncan2  13861  ablpnpcan  13865  ablnncan  13866  invghm  13874  gsumfzconst  13886  gsumfzsnfd  13890  rngm2neg  13920  srgpcompp  13962  srgpcomppsc  13963  ringinvnzdiv  14021  ringm2neg  14026  dvr1  14110  dvrcan1  14112  dvrcan3  14113  rdivmuldivd  14116  lmodfopne  14298  sralemg  14410  gsumfzfsumlemm  14559  mplsubgfilemcl  14671  mplsubgfileminv  14672  xmetxpbl  15190  ivthinclemuopn  15320  limcimolemlt  15346  cnplimcim  15349  limccnpcntop  15357  limccnp2lem  15358  dvexp  15393  dvmptcmulcn  15403  dvply1  15447  ef2kpi  15488  sinhalfpip  15502  sinhalfpim  15503  coshalfpim  15505  ptolemy  15506  tangtx  15520  rpabscxpbnd  15622  relogbexpap  15640  rplogbcxp  15645  rpcxplogb  15646  binom4  15661  wilthlem1  15662  0sgm  15667  mpodvdsmulf1o  15672  fsumdvdsmul  15673  sgmppw  15674  0sgmppw  15675  1sgm2ppw  15677  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsval2lem  15697  lgsval4  15707  lgsval4a  15709  lgsneg  15711  lgsneg1  15712  lgsdirprm  15721  lgsdir  15722  lgsne0  15725  lgsmulsqcoprm  15733  gausslemma2dlem1a  15745  gausslemma2dlem6  15754  gausslemma2d  15756  lgseisenlem3  15759  lgseisenlem4  15760  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem1  15768  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgslem3d1  15787  2sqlem3  15804  structiedg0val  15849  uhgr2edg  16012  edginwlkd  16076  peano4nninf  16399  trilpolemclim  16431  trilpolemeq1  16435  apdifflemf  16441