Theorem 3eqtrd 2269

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 2265	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	1, 4	eqtrd 2265	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  tpeq123d  3783  diftpsn3  3835  oteq123d  3898  resiima  5120  fvun1  5743  fvmptd  5758  fmptpr  5876  caovlem2d  6247  offval  6274  ofvalg  6276  cnvf1olem  6420  supp0  6438  suppsnopdc  6450  suppofss1dcl  6464  suppofss2dcl  6465  suppcofn  6466  nnm1  6758  updjudhcoinlf  7371  updjudhcoinrg  7372  caseinl  7382  caseinr  7383  omp1eomlem  7385  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  ltexnqq  7723  prarloclemarch  7733  ltrnqg  7735  nq02m  7780  prarloclemcalc  7817  mulnqprl  7883  mulnqpru  7884  ltexprlemloc  7922  addcanprleml  7929  recexprlem1ssu  7949  cauappcvgprlem1  7974  caucvgsrlemfv  8106  caucvgsrlemoffval  8111  recidpirqlemcalc  8172  axmulass  8188  axrnegex  8194  muladd11r  8429  addcan2  8454  addsub  8484  subsub2  8501  negsubdi2  8532  muladd  8657  mulsub  8674  cru  8876  mulreim  8878  recextlem1  8925  mulap0  8928  muleqadd  8942  divrecap  8962  div23ap  8965  div12ap  8968  divmulasscomap  8970  divcanap7  8995  conjmulap  9003  apmul1  9062  nndivtr  9279  subhalfhalf  9473  xp1d2m1eqxm1d2  9491  div4p1lem1div2  9492  qapne  9971  xnegneg  10166  rexsub  10186  xnegid  10192  fseq1p1m1  10428  nn0split  10470  nnsplit  10471  fzosplitsnm1  10554  fzosplitpr  10579  fzosplitprm1  10580  ceilid  10677  flqdiv  10683  zmod10  10702  modqcyc  10721  modqaddabs  10724  mulqaddmodid  10726  modqadd2mod  10736  modqm1p1mod0  10737  modqmul12d  10740  modqadd12d  10742  modqmulmodr  10752  modqaddmulmod  10753  frecuzrdgsuc  10776  seqeq123d  10818  seqvalcd  10823  seq3f1olemqsumkj  10873  seq3f1oleml  10878  seqf1oglem2  10882  seq3id3  10886  seq3id  10887  seq3homo  10889  seq3z  10890  seqhomog  10892  exp1  10907  expnegap0  10909  expmulzap  10947  m1expeven  10948  expdivap  10952  binom3  11019  sqoddm1div8  11055  mulsubdivbinom2ap  11073  bcn1  11120  bcnp1n  11121  bcval5  11125  bcn2m1  11132  bcn2p1  11133  hashdifpr  11185  hashmap  11192  hashfibclem  11206  ccatlen  11283  ccatalpha  11301  ccatw2s1leng  11326  ccats1val2  11328  lswccats1  11331  swrdlend  11350  ccatswrd  11362  pfxmpt  11372  pfxfv  11376  pfxfvlsw  11387  ccatpfx  11393  pfx1  11395  pfxswrd  11398  swrdpfx  11399  pfxpfx  11400  lenrevpfxcctswrd  11404  wrdind  11414  wrd2ind  11415  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatpfx2  11429  pfxccatid  11433  cats1fvnd  11457  crim  11543  remullem  11556  remul2  11558  immul2  11565  ipcnval  11571  cjreim  11588  recvguniqlem  11679  resqrexlemover  11695  resqrexlemcalc1  11699  absid  11756  amgm2  11803  max0addsup  11904  minabs  11921  xrmaxrecl  11940  xrminadd  11960  fsumsplitf  12094  sumsnf  12095  fsump1i  12119  fsum2dlemstep  12120  fsumshftm  12131  fsummulc2  12134  modfsummodlemstep  12143  telfsumo  12152  fsumrelem  12157  hash2iun1dif1  12166  binomlem  12169  binom1dif  12173  arisum  12184  geo2sum  12200  geo2sum2  12201  cvgratz  12218  mertenslemi1  12221  clim2prod  12225  fprodeq0  12303  fprod2dlemstep  12308  fproddivap  12316  fproddivapf  12317  fprodmodd  12327  ef0lem  12346  eftlub  12376  efsep  12377  effsumlt  12378  tanval2ap  12399  efi4p  12403  resin4p  12404  recos4p  12405  efeul  12420  sinadd  12422  cosadd  12423  sinmul  12430  ef01bndlem  12442  cos12dec  12454  absef  12456  demoivreALT  12460  dvds2ln  12510  dvdseq  12534  opeo  12583  bezoutlemnewy  12692  nninfctlemfo  12736  eucalginv  12753  eucalglt  12754  eucalg  12756  lcmgcdlem  12774  lcm1  12778  divgcdcoprmex  12799  2sqpwodd  12873  zgcdsq  12898  qden1elz  12902  phiprmpw  12919  eulerthlem1  12924  eulerthlemrprm  12926  prmdiv  12932  hashgcdlem  12935  odzdvds  12943  vfermltl  12949  modprm0  12952  pythagtriplem12  12973  pcqmul  13001  pcaddlem  13037  pcadd  13038  pcadd2  13039  pcmpt  13041  pcmpt2  13042  mul4sqlem  13091  4sqlem11  13099  4sqlem17  13105  nninfdclemp1  13201  ressressg  13288  gsumsplit1r  13611  gsumprval  13612  mndinvmod  13658  mhmco  13703  gsumfzz  13708  grpinvid2  13766  grpasscan2  13777  grpinvssd  13790  grpinvadd  13791  grpsubid1  13798  grpsubadd  13801  grppncan  13804  mulg1  13846  mulgaddcomlem  13862  mulgdirlem  13870  mulgneg2  13873  mulgmodid  13878  nmzsubg  13927  qusinv  13953  qussub  13954  conjnmz  13996  ablsub2inv  14028  abladdsub4  14031  abladdsub  14032  ablpncan2  14033  ablpnpcan  14037  ablnncan  14038  invghm  14046  gsumfzconst  14058  gsumfzsnfd  14062  rngm2neg  14093  srgpcompp  14135  srgpcomppsc  14136  ringinvnzdiv  14194  ringm2neg  14199  dvr1  14283  dvrcan1  14285  dvrcan3  14286  rdivmuldivd  14289  lmodfopne  14474  sralemg  14586  gsumfzfsumlemm  14735  mplsubgfilemcl  14854  mplsubgfileminv  14855  xmetxpbl  15373  ivthinclemuopn  15503  limcimolemlt  15529  cnplimcim  15532  limccnpcntop  15540  limccnp2lem  15541  dvexp  15576  dvmptcmulcn  15586  dvply1  15630  ef2kpi  15671  sinhalfpip  15685  sinhalfpim  15686  coshalfpim  15688  ptolemy  15689  tangtx  15703  rpabscxpbnd  15805  relogbexpap  15823  rplogbcxp  15828  rpcxplogb  15829  binom4  15844  pellexlem2  15846  wilthlem1  15848  0sgm  15853  mpodvdsmulf1o  15858  fsumdvdsmul  15859  sgmppw  15860  0sgmppw  15861  1sgm2ppw  15863  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsval2lem  15883  lgsval4  15893  lgsval4a  15895  lgsneg  15897  lgsneg1  15898  lgsdirprm  15907  lgsdir  15908  lgsne0  15911  lgsmulsqcoprm  15919  gausslemma2dlem1a  15931  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3d1  15973  2sqlem3  15990  structiedg0val  16035  uhgr2edg  16201  usgr1e  16236  vtxdgfifival  16286  vtxdfifiun  16292  vtxdumgrfival  16293  vtxduspgrfvedgfi  16296  1loopgredg  16299  1loopgrvd2fi  16300  1hevtxdg1en  16303  p1evtxdeqfi  16307  edginwlkd  16350  clwwlknonex2lem1  16432  eupthvdres  16470  peano4nninf  16784  repiecele0  16810  repiecege0  16811  trilpolemclim  16820  trilpolemeq1  16824  apdifflemf  16830  gfsumval  16862  gfsumsn  16867  gfsumz  16869