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  7258  updjudhcoinrg  7259  caseinl  7269  caseinr  7270  omp1eomlem  7272  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  ltexnqq  7606  prarloclemarch  7616  ltrnqg  7618  nq02m  7663  prarloclemcalc  7700  mulnqprl  7766  mulnqpru  7767  ltexprlemloc  7805  addcanprleml  7812  recexprlem1ssu  7832  cauappcvgprlem1  7857  caucvgsrlemfv  7989  caucvgsrlemoffval  7994  recidpirqlemcalc  8055  axmulass  8071  axrnegex  8077  muladd11r  8313  addcan2  8338  addsub  8368  subsub2  8385  negsubdi2  8416  muladd  8541  mulsub  8558  cru  8760  mulreim  8762  recextlem1  8809  mulap0  8812  muleqadd  8826  divrecap  8846  div23ap  8849  div12ap  8852  divmulasscomap  8854  divcanap7  8879  conjmulap  8887  apmul1  8946  nndivtr  9163  subhalfhalf  9357  xp1d2m1eqxm1d2  9375  div4p1lem1div2  9376  qapne  9846  xnegneg  10041  rexsub  10061  xnegid  10067  fseq1p1m1  10302  nn0split  10344  nnsplit  10345  fzosplitsnm1  10427  fzosplitprm1  10452  ceilid  10549  flqdiv  10555  zmod10  10574  modqcyc  10593  modqaddabs  10596  mulqaddmodid  10598  modqadd2mod  10608  modqm1p1mod0  10609  modqmul12d  10612  modqadd12d  10614  modqmulmodr  10624  modqaddmulmod  10625  frecuzrdgsuc  10648  seqeq123d  10690  seqvalcd  10695  seq3f1olemqsumkj  10745  seq3f1oleml  10750  seqf1oglem2  10754  seq3id3  10758  seq3id  10759  seq3homo  10761  seq3z  10762  seqhomog  10764  exp1  10779  expnegap0  10781  expmulzap  10819  m1expeven  10820  expdivap  10824  binom3  10891  sqoddm1div8  10927  mulsubdivbinom2ap  10945  bcn1  10992  bcnp1n  10993  bcval5  10997  bcn2m1  11003  bcn2p1  11004  hashdifpr  11055  ccatlen  11143  ccatalpha  11161  ccats1val2  11186  lswccats1  11189  swrdlend  11205  ccatswrd  11217  pfxmpt  11227  pfxfv  11231  pfxfvlsw  11242  ccatpfx  11248  pfx1  11250  pfxswrd  11253  swrdpfx  11254  pfxpfx  11255  lenrevpfxcctswrd  11259  wrdind  11269  wrd2ind  11270  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatpfx2  11284  pfxccatid  11288  cats1fvnd  11312  crim  11384  remullem  11397  remul2  11399  immul2  11406  ipcnval  11412  cjreim  11429  recvguniqlem  11520  resqrexlemover  11536  resqrexlemcalc1  11540  absid  11597  amgm2  11644  max0addsup  11745  minabs  11762  xrmaxrecl  11781  xrminadd  11801  fsumsplitf  11934  sumsnf  11935  fsump1i  11959  fsum2dlemstep  11960  fsumshftm  11971  fsummulc2  11974  modfsummodlemstep  11983  telfsumo  11992  fsumrelem  11997  hash2iun1dif1  12006  binomlem  12009  binom1dif  12013  arisum  12024  geo2sum  12040  geo2sum2  12041  cvgratz  12058  mertenslemi1  12061  clim2prod  12065  fprodeq0  12143  fprod2dlemstep  12148  fproddivap  12156  fproddivapf  12157  fprodmodd  12167  ef0lem  12186  eftlub  12216  efsep  12217  effsumlt  12218  tanval2ap  12239  efi4p  12243  resin4p  12244  recos4p  12245  efeul  12260  sinadd  12262  cosadd  12263  sinmul  12270  ef01bndlem  12282  cos12dec  12294  absef  12296  demoivreALT  12300  dvds2ln  12350  dvdseq  12374  opeo  12423  bezoutlemnewy  12532  nninfctlemfo  12576  eucalginv  12593  eucalglt  12594  eucalg  12596  lcmgcdlem  12614  lcm1  12618  divgcdcoprmex  12639  2sqpwodd  12713  zgcdsq  12738  qden1elz  12742  phiprmpw  12759  eulerthlem1  12764  eulerthlemrprm  12766  prmdiv  12772  hashgcdlem  12775  odzdvds  12783  vfermltl  12789  modprm0  12792  pythagtriplem12  12813  pcqmul  12841  pcaddlem  12877  pcadd  12878  pcadd2  12879  pcmpt  12881  pcmpt2  12882  mul4sqlem  12931  4sqlem11  12939  4sqlem17  12945  nninfdclemp1  13036  ressressg  13123  gsumsplit1r  13446  gsumprval  13447  mndinvmod  13493  mhmco  13538  gsumfzz  13543  grpinvid2  13601  grpasscan2  13612  grpinvssd  13625  grpinvadd  13626  grpsubid1  13633  grpsubadd  13636  grppncan  13639  mulg1  13681  mulgaddcomlem  13697  mulgdirlem  13705  mulgneg2  13708  mulgmodid  13713  nmzsubg  13762  qusinv  13788  qussub  13789  conjnmz  13831  ablsub2inv  13863  abladdsub4  13866  abladdsub  13867  ablpncan2  13868  ablpnpcan  13872  ablnncan  13873  invghm  13881  gsumfzconst  13893  gsumfzsnfd  13897  rngm2neg  13927  srgpcompp  13969  srgpcomppsc  13970  ringinvnzdiv  14028  ringm2neg  14033  dvr1  14117  dvrcan1  14119  dvrcan3  14120  rdivmuldivd  14123  lmodfopne  14305  sralemg  14417  gsumfzfsumlemm  14566  mplsubgfilemcl  14678  mplsubgfileminv  14679  xmetxpbl  15197  ivthinclemuopn  15327  limcimolemlt  15353  cnplimcim  15356  limccnpcntop  15364  limccnp2lem  15365  dvexp  15400  dvmptcmulcn  15410  dvply1  15454  ef2kpi  15495  sinhalfpip  15509  sinhalfpim  15510  coshalfpim  15512  ptolemy  15513  tangtx  15527  rpabscxpbnd  15629  relogbexpap  15647  rplogbcxp  15652  rpcxplogb  15653  binom4  15668  wilthlem1  15669  0sgm  15674  mpodvdsmulf1o  15679  fsumdvdsmul  15680  sgmppw  15681  0sgmppw  15682  1sgm2ppw  15684  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsval2lem  15704  lgsval4  15714  lgsval4a  15716  lgsneg  15718  lgsneg1  15719  lgsdirprm  15728  lgsdir  15729  lgsne0  15732  lgsmulsqcoprm  15740  gausslemma2dlem1a  15752  gausslemma2dlem6  15761  gausslemma2d  15763  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgslem3d1  15794  2sqlem3  15811  structiedg0val  15856  uhgr2edg  16019  vtxdgfifival  16050  vtxdfifiun  16056  vtxdumgrfival  16057  edginwlkd  16096  peano4nninf  16432  trilpolemclim  16464  trilpolemeq1  16468  apdifflemf  16474