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  3808  oteq123d  3871  resiima  5085  fvun1  5699  fvmptd  5714  fmptpr  5830  caovlem2d  6197  offval  6224  ofvalg  6226  cnvf1olem  6368  nnm1  6669  updjudhcoinlf  7243  updjudhcoinrg  7244  caseinl  7254  caseinr  7255  omp1eomlem  7257  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  ltexnqq  7591  prarloclemarch  7601  ltrnqg  7603  nq02m  7648  prarloclemcalc  7685  mulnqprl  7751  mulnqpru  7752  ltexprlemloc  7790  addcanprleml  7797  recexprlem1ssu  7817  cauappcvgprlem1  7842  caucvgsrlemfv  7974  caucvgsrlemoffval  7979  recidpirqlemcalc  8040  axmulass  8056  axrnegex  8062  muladd11r  8298  addcan2  8323  addsub  8353  subsub2  8370  negsubdi2  8401  muladd  8526  mulsub  8543  cru  8745  mulreim  8747  recextlem1  8794  mulap0  8797  muleqadd  8811  divrecap  8831  div23ap  8834  div12ap  8837  divmulasscomap  8839  divcanap7  8864  conjmulap  8872  apmul1  8931  nndivtr  9148  subhalfhalf  9342  xp1d2m1eqxm1d2  9360  div4p1lem1div2  9361  qapne  9830  xnegneg  10025  rexsub  10045  xnegid  10051  fseq1p1m1  10286  nn0split  10328  nnsplit  10329  fzosplitsnm1  10410  fzosplitprm1  10435  ceilid  10532  flqdiv  10538  zmod10  10557  modqcyc  10576  modqaddabs  10579  mulqaddmodid  10581  modqadd2mod  10591  modqm1p1mod0  10592  modqmul12d  10595  modqadd12d  10597  modqmulmodr  10607  modqaddmulmod  10608  frecuzrdgsuc  10631  seqeq123d  10673  seqvalcd  10678  seq3f1olemqsumkj  10728  seq3f1oleml  10733  seqf1oglem2  10737  seq3id3  10741  seq3id  10742  seq3homo  10744  seq3z  10745  seqhomog  10747  exp1  10762  expnegap0  10764  expmulzap  10802  m1expeven  10803  expdivap  10807  binom3  10874  sqoddm1div8  10910  mulsubdivbinom2ap  10928  bcn1  10975  bcnp1n  10976  bcval5  10980  bcn2m1  10986  bcn2p1  10987  hashdifpr  11037  ccatlen  11125  ccats1val2  11166  lswccats1  11169  swrdlend  11185  ccatswrd  11197  pfxmpt  11207  pfxfv  11211  pfxfvlsw  11222  ccatpfx  11228  pfx1  11230  pfxswrd  11233  swrdpfx  11234  pfxpfx  11235  lenrevpfxcctswrd  11239  wrdind  11249  wrd2ind  11250  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatpfx2  11264  pfxccatid  11268  cats1fvnd  11292  crim  11364  remullem  11377  remul2  11379  immul2  11386  ipcnval  11392  cjreim  11409  recvguniqlem  11500  resqrexlemover  11516  resqrexlemcalc1  11520  absid  11577  amgm2  11624  max0addsup  11725  minabs  11742  xrmaxrecl  11761  xrminadd  11781  fsumsplitf  11914  sumsnf  11915  fsump1i  11939  fsum2dlemstep  11940  fsumshftm  11951  fsummulc2  11954  modfsummodlemstep  11963  telfsumo  11972  fsumrelem  11977  hash2iun1dif1  11986  binomlem  11989  binom1dif  11993  arisum  12004  geo2sum  12020  geo2sum2  12021  cvgratz  12038  mertenslemi1  12041  clim2prod  12045  fprodeq0  12123  fprod2dlemstep  12128  fproddivap  12136  fproddivapf  12137  fprodmodd  12147  ef0lem  12166  eftlub  12196  efsep  12197  effsumlt  12198  tanval2ap  12219  efi4p  12223  resin4p  12224  recos4p  12225  efeul  12240  sinadd  12242  cosadd  12243  sinmul  12250  ef01bndlem  12262  cos12dec  12274  absef  12276  demoivreALT  12280  dvds2ln  12330  dvdseq  12354  opeo  12403  bezoutlemnewy  12512  nninfctlemfo  12556  eucalginv  12573  eucalglt  12574  eucalg  12576  lcmgcdlem  12594  lcm1  12598  divgcdcoprmex  12619  2sqpwodd  12693  zgcdsq  12718  qden1elz  12722  phiprmpw  12739  eulerthlem1  12744  eulerthlemrprm  12746  prmdiv  12752  hashgcdlem  12755  odzdvds  12763  vfermltl  12769  modprm0  12772  pythagtriplem12  12793  pcqmul  12821  pcaddlem  12857  pcadd  12858  pcadd2  12859  pcmpt  12861  pcmpt2  12862  mul4sqlem  12911  4sqlem11  12919  4sqlem17  12925  nninfdclemp1  13016  ressressg  13103  gsumsplit1r  13426  gsumprval  13427  mndinvmod  13473  mhmco  13518  gsumfzz  13523  grpinvid2  13581  grpasscan2  13592  grpinvssd  13605  grpinvadd  13606  grpsubid1  13613  grpsubadd  13616  grppncan  13619  mulg1  13661  mulgaddcomlem  13677  mulgdirlem  13685  mulgneg2  13688  mulgmodid  13693  nmzsubg  13742  qusinv  13768  qussub  13769  conjnmz  13811  ablsub2inv  13843  abladdsub4  13846  abladdsub  13847  ablpncan2  13848  ablpnpcan  13852  ablnncan  13853  invghm  13861  gsumfzconst  13873  gsumfzsnfd  13877  rngm2neg  13907  srgpcompp  13949  srgpcomppsc  13950  ringinvnzdiv  14008  ringm2neg  14013  dvr1  14096  dvrcan1  14098  dvrcan3  14099  rdivmuldivd  14102  lmodfopne  14284  sralemg  14396  gsumfzfsumlemm  14545  mplsubgfilemcl  14657  mplsubgfileminv  14658  xmetxpbl  15176  ivthinclemuopn  15306  limcimolemlt  15332  cnplimcim  15335  limccnpcntop  15343  limccnp2lem  15344  dvexp  15379  dvmptcmulcn  15389  dvply1  15433  ef2kpi  15474  sinhalfpip  15488  sinhalfpim  15489  coshalfpim  15491  ptolemy  15492  tangtx  15506  rpabscxpbnd  15608  relogbexpap  15626  rplogbcxp  15631  rpcxplogb  15632  binom4  15647  wilthlem1  15648  0sgm  15653  mpodvdsmulf1o  15658  fsumdvdsmul  15659  sgmppw  15660  0sgmppw  15661  1sgm2ppw  15663  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsval2lem  15683  lgsval4  15693  lgsval4a  15695  lgsneg  15697  lgsneg1  15698  lgsdirprm  15707  lgsdir  15708  lgsne0  15711  lgsmulsqcoprm  15719  gausslemma2dlem1a  15731  gausslemma2dlem6  15740  gausslemma2d  15742  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2sqlem3  15790  structiedg0val  15835  uhgr2edg  15998  peano4nninf  16331  trilpolemclim  16363  trilpolemeq1  16367  apdifflemf  16373