Theorem 3eqtrd 2268

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  tpeq123d  3763  diftpsn3  3814  oteq123d  3877  resiima  5094  fvun1  5712  fvmptd  5727  fmptpr  5845  caovlem2d  6214  offval  6242  ofvalg  6244  cnvf1olem  6388  nnm1  6692  updjudhcoinlf  7278  updjudhcoinrg  7279  caseinl  7289  caseinr  7290  omp1eomlem  7292  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  ltexnqq  7627  prarloclemarch  7637  ltrnqg  7639  nq02m  7684  prarloclemcalc  7721  mulnqprl  7787  mulnqpru  7788  ltexprlemloc  7826  addcanprleml  7833  recexprlem1ssu  7853  cauappcvgprlem1  7878  caucvgsrlemfv  8010  caucvgsrlemoffval  8015  recidpirqlemcalc  8076  axmulass  8092  axrnegex  8098  muladd11r  8334  addcan2  8359  addsub  8389  subsub2  8406  negsubdi2  8437  muladd  8562  mulsub  8579  cru  8781  mulreim  8783  recextlem1  8830  mulap0  8833  muleqadd  8847  divrecap  8867  div23ap  8870  div12ap  8873  divmulasscomap  8875  divcanap7  8900  conjmulap  8908  apmul1  8967  nndivtr  9184  subhalfhalf  9378  xp1d2m1eqxm1d2  9396  div4p1lem1div2  9397  qapne  9872  xnegneg  10067  rexsub  10087  xnegid  10093  fseq1p1m1  10328  nn0split  10370  nnsplit  10371  fzosplitsnm1  10453  fzosplitpr  10478  fzosplitprm1  10479  ceilid  10576  flqdiv  10582  zmod10  10601  modqcyc  10620  modqaddabs  10623  mulqaddmodid  10625  modqadd2mod  10635  modqm1p1mod0  10636  modqmul12d  10639  modqadd12d  10641  modqmulmodr  10651  modqaddmulmod  10652  frecuzrdgsuc  10675  seqeq123d  10717  seqvalcd  10722  seq3f1olemqsumkj  10772  seq3f1oleml  10777  seqf1oglem2  10781  seq3id3  10785  seq3id  10786  seq3homo  10788  seq3z  10789  seqhomog  10791  exp1  10806  expnegap0  10808  expmulzap  10846  m1expeven  10847  expdivap  10851  binom3  10918  sqoddm1div8  10954  mulsubdivbinom2ap  10972  bcn1  11019  bcnp1n  11020  bcval5  11024  bcn2m1  11030  bcn2p1  11031  hashdifpr  11083  ccatlen  11171  ccatalpha  11189  ccatw2s1leng  11214  ccats1val2  11216  lswccats1  11219  swrdlend  11238  ccatswrd  11250  pfxmpt  11260  pfxfv  11264  pfxfvlsw  11275  ccatpfx  11281  pfx1  11283  pfxswrd  11286  swrdpfx  11287  pfxpfx  11288  lenrevpfxcctswrd  11292  wrdind  11302  wrd2ind  11303  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatpfx2  11317  pfxccatid  11321  cats1fvnd  11345  crim  11418  remullem  11431  remul2  11433  immul2  11440  ipcnval  11446  cjreim  11463  recvguniqlem  11554  resqrexlemover  11570  resqrexlemcalc1  11574  absid  11631  amgm2  11678  max0addsup  11779  minabs  11796  xrmaxrecl  11815  xrminadd  11835  fsumsplitf  11968  sumsnf  11969  fsump1i  11993  fsum2dlemstep  11994  fsumshftm  12005  fsummulc2  12008  modfsummodlemstep  12017  telfsumo  12026  fsumrelem  12031  hash2iun1dif1  12040  binomlem  12043  binom1dif  12047  arisum  12058  geo2sum  12074  geo2sum2  12075  cvgratz  12092  mertenslemi1  12095  clim2prod  12099  fprodeq0  12177  fprod2dlemstep  12182  fproddivap  12190  fproddivapf  12191  fprodmodd  12201  ef0lem  12220  eftlub  12250  efsep  12251  effsumlt  12252  tanval2ap  12273  efi4p  12277  resin4p  12278  recos4p  12279  efeul  12294  sinadd  12296  cosadd  12297  sinmul  12304  ef01bndlem  12316  cos12dec  12328  absef  12330  demoivreALT  12334  dvds2ln  12384  dvdseq  12408  opeo  12457  bezoutlemnewy  12566  nninfctlemfo  12610  eucalginv  12627  eucalglt  12628  eucalg  12630  lcmgcdlem  12648  lcm1  12652  divgcdcoprmex  12673  2sqpwodd  12747  zgcdsq  12772  qden1elz  12776  phiprmpw  12793  eulerthlem1  12798  eulerthlemrprm  12800  prmdiv  12806  hashgcdlem  12809  odzdvds  12817  vfermltl  12823  modprm0  12826  pythagtriplem12  12847  pcqmul  12875  pcaddlem  12911  pcadd  12912  pcadd2  12913  pcmpt  12915  pcmpt2  12916  mul4sqlem  12965  4sqlem11  12973  4sqlem17  12979  nninfdclemp1  13070  ressressg  13157  gsumsplit1r  13480  gsumprval  13481  mndinvmod  13527  mhmco  13572  gsumfzz  13577  grpinvid2  13635  grpasscan2  13646  grpinvssd  13659  grpinvadd  13660  grpsubid1  13667  grpsubadd  13670  grppncan  13673  mulg1  13715  mulgaddcomlem  13731  mulgdirlem  13739  mulgneg2  13742  mulgmodid  13747  nmzsubg  13796  qusinv  13822  qussub  13823  conjnmz  13865  ablsub2inv  13897  abladdsub4  13900  abladdsub  13901  ablpncan2  13902  ablpnpcan  13906  ablnncan  13907  invghm  13915  gsumfzconst  13927  gsumfzsnfd  13931  rngm2neg  13961  srgpcompp  14003  srgpcomppsc  14004  ringinvnzdiv  14062  ringm2neg  14067  dvr1  14151  dvrcan1  14153  dvrcan3  14154  rdivmuldivd  14157  lmodfopne  14339  sralemg  14451  gsumfzfsumlemm  14600  mplsubgfilemcl  14712  mplsubgfileminv  14713  xmetxpbl  15231  ivthinclemuopn  15361  limcimolemlt  15387  cnplimcim  15390  limccnpcntop  15398  limccnp2lem  15399  dvexp  15434  dvmptcmulcn  15444  dvply1  15488  ef2kpi  15529  sinhalfpip  15543  sinhalfpim  15544  coshalfpim  15546  ptolemy  15547  tangtx  15561  rpabscxpbnd  15663  relogbexpap  15681  rplogbcxp  15686  rpcxplogb  15687  binom4  15702  wilthlem1  15703  0sgm  15708  mpodvdsmulf1o  15713  fsumdvdsmul  15714  sgmppw  15715  0sgmppw  15716  1sgm2ppw  15718  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsval2lem  15738  lgsval4  15748  lgsval4a  15750  lgsneg  15752  lgsneg1  15753  lgsdirprm  15762  lgsdir  15763  lgsne0  15766  lgsmulsqcoprm  15774  gausslemma2dlem1a  15786  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3d1  15828  2sqlem3  15845  structiedg0val  15890  uhgr2edg  16056  usgr1e  16091  vtxdgfifival  16141  vtxdfifiun  16147  vtxdumgrfival  16148  vtxduspgrfvedgfi  16151  1loopgredg  16154  1loopgrvd2fi  16155  1hevtxdg1en  16158  p1evtxdeqfi  16162  edginwlkd  16205  clwwlknonex2lem1  16287  peano4nninf  16608  trilpolemclim  16640  trilpolemeq1  16644  apdifflemf  16650  gfsumval  16680