Theorem 3eqtrd 2230

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  tpeq123d  3710  diftpsn3  3759  oteq123d  3819  resiima  5023  fvun1  5623  fvmptd  5638  fmptpr  5750  caovlem2d  6111  offval  6138  ofvalg  6140  cnvf1olem  6277  nnm1  6578  updjudhcoinlf  7139  updjudhcoinrg  7140  caseinl  7150  caseinr  7151  omp1eomlem  7153  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  ltexnqq  7468  prarloclemarch  7478  ltrnqg  7480  nq02m  7525  prarloclemcalc  7562  mulnqprl  7628  mulnqpru  7629  ltexprlemloc  7667  addcanprleml  7674  recexprlem1ssu  7694  cauappcvgprlem1  7719  caucvgsrlemfv  7851  caucvgsrlemoffval  7856  recidpirqlemcalc  7917  axmulass  7933  axrnegex  7939  muladd11r  8175  addcan2  8200  addsub  8230  subsub2  8247  negsubdi2  8278  muladd  8403  mulsub  8420  cru  8621  mulreim  8623  recextlem1  8670  mulap0  8673  muleqadd  8687  divrecap  8707  div23ap  8710  div12ap  8713  divmulasscomap  8715  divcanap7  8740  conjmulap  8748  apmul1  8807  nndivtr  9024  subhalfhalf  9217  xp1d2m1eqxm1d2  9235  div4p1lem1div2  9236  qapne  9704  xnegneg  9899  rexsub  9919  xnegid  9925  fseq1p1m1  10160  nn0split  10202  nnsplit  10203  fzosplitsnm1  10276  fzosplitprm1  10301  ceilid  10386  flqdiv  10392  zmod10  10411  modqcyc  10430  modqaddabs  10433  mulqaddmodid  10435  modqadd2mod  10445  modqm1p1mod0  10446  modqmul12d  10449  modqadd12d  10451  modqmulmodr  10461  modqaddmulmod  10462  frecuzrdgsuc  10485  seqeq123d  10527  seqvalcd  10532  seq3f1olemqsumkj  10582  seq3f1oleml  10587  seqf1oglem2  10591  seq3id3  10595  seq3id  10596  seq3homo  10598  seq3z  10599  seqhomog  10601  exp1  10616  expnegap0  10618  expmulzap  10656  m1expeven  10657  expdivap  10661  binom3  10728  sqoddm1div8  10764  mulsubdivbinom2ap  10782  bcn1  10829  bcnp1n  10830  bcval5  10834  bcn2m1  10840  bcn2p1  10841  hashdifpr  10891  crim  11002  remullem  11015  remul2  11017  immul2  11024  ipcnval  11030  cjreim  11047  recvguniqlem  11138  resqrexlemover  11154  resqrexlemcalc1  11158  absid  11215  amgm2  11262  max0addsup  11363  minabs  11379  xrmaxrecl  11398  xrminadd  11418  fsumsplitf  11551  sumsnf  11552  fsump1i  11576  fsum2dlemstep  11577  fsumshftm  11588  fsummulc2  11591  modfsummodlemstep  11600  telfsumo  11609  fsumrelem  11614  hash2iun1dif1  11623  binomlem  11626  binom1dif  11630  arisum  11641  geo2sum  11657  geo2sum2  11658  cvgratz  11675  mertenslemi1  11678  clim2prod  11682  fprodeq0  11760  fprod2dlemstep  11765  fproddivap  11773  fproddivapf  11774  fprodmodd  11784  ef0lem  11803  eftlub  11833  efsep  11834  effsumlt  11835  tanval2ap  11856  efi4p  11860  resin4p  11861  recos4p  11862  efeul  11877  sinadd  11879  cosadd  11880  sinmul  11887  ef01bndlem  11899  cos12dec  11911  absef  11913  demoivreALT  11917  dvds2ln  11967  dvdseq  11990  opeo  12038  bezoutlemnewy  12133  nninfctlemfo  12177  eucalginv  12194  eucalglt  12195  eucalg  12197  lcmgcdlem  12215  lcm1  12219  divgcdcoprmex  12240  2sqpwodd  12314  zgcdsq  12339  qden1elz  12343  phiprmpw  12360  eulerthlem1  12365  eulerthlemrprm  12367  prmdiv  12373  hashgcdlem  12376  odzdvds  12383  vfermltl  12389  modprm0  12392  pythagtriplem12  12413  pcqmul  12441  pcaddlem  12477  pcadd  12478  pcadd2  12479  pcmpt  12481  pcmpt2  12482  mul4sqlem  12531  4sqlem11  12539  4sqlem17  12545  nninfdclemp1  12607  ressressg  12693  gsumsplit1r  12981  gsumprval  12982  mndinvmod  13026  mhmco  13062  gsumfzz  13067  grpinvid2  13125  grpasscan2  13136  grpinvssd  13149  grpinvadd  13150  grpsubid1  13157  grpsubadd  13160  grppncan  13163  mulg1  13199  mulgaddcomlem  13215  mulgdirlem  13223  mulgneg2  13226  mulgmodid  13231  nmzsubg  13280  qusinv  13306  qussub  13307  conjnmz  13349  ablsub2inv  13381  abladdsub4  13384  abladdsub  13385  ablpncan2  13386  ablpnpcan  13390  ablnncan  13391  invghm  13399  gsumfzconst  13411  gsumfzsnfd  13415  rngm2neg  13445  srgpcompp  13487  srgpcomppsc  13488  ringinvnzdiv  13546  ringm2neg  13551  dvr1  13634  dvrcan1  13636  dvrcan3  13637  rdivmuldivd  13640  lmodfopne  13822  sralemg  13934  gsumfzfsumlemm  14075  xmetxpbl  14676  ivthinclemuopn  14792  limcimolemlt  14818  cnplimcim  14821  limccnpcntop  14829  limccnp2lem  14830  dvexp  14860  dvmptcmulcn  14868  ef2kpi  14941  sinhalfpip  14955  sinhalfpim  14956  coshalfpim  14958  ptolemy  14959  tangtx  14973  rpabscxpbnd  15073  relogbexpap  15090  rplogbcxp  15095  rpcxplogb  15096  binom4  15111  wilthlem1  15112  lgsval2lem  15126  lgsval4  15136  lgsval4a  15138  lgsneg  15140  lgsneg1  15141  lgsdirprm  15150  lgsdir  15151  lgsne0  15154  lgsmulsqcoprm  15162  gausslemma2dlem1a  15174  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  2sqlem3  15204  peano4nninf  15496  trilpolemclim  15526  trilpolemeq1  15530  apdifflemf  15536