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 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 2213

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

This theorem is referenced by:  tpeq123d  3767  diftpsn3  3819  oteq123d  3882  resiima  5101  fvun1  5721  fvmptd  5736  fmptpr  5854  caovlem2d  6225  offval  6252  ofvalg  6254  cnvf1olem  6398  supp0  6416  suppsnopdc  6428  suppofss1dcl  6442  suppofss2dcl  6443  suppcofn  6444  nnm1  6736  updjudhcoinlf  7322  updjudhcoinrg  7323  caseinl  7333  caseinr  7334  omp1eomlem  7336  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  ltexnqq  7671  prarloclemarch  7681  ltrnqg  7683  nq02m  7728  prarloclemcalc  7765  mulnqprl  7831  mulnqpru  7832  ltexprlemloc  7870  addcanprleml  7877  recexprlem1ssu  7897  cauappcvgprlem1  7922  caucvgsrlemfv  8054  caucvgsrlemoffval  8059  recidpirqlemcalc  8120  axmulass  8136  axrnegex  8142  muladd11r  8377  addcan2  8402  addsub  8432  subsub2  8449  negsubdi2  8480  muladd  8605  mulsub  8622  cru  8824  mulreim  8826  recextlem1  8873  mulap0  8876  muleqadd  8890  divrecap  8910  div23ap  8913  div12ap  8916  divmulasscomap  8918  divcanap7  8943  conjmulap  8951  apmul1  9010  nndivtr  9227  subhalfhalf  9421  xp1d2m1eqxm1d2  9439  div4p1lem1div2  9440  qapne  9917  xnegneg  10112  rexsub  10132  xnegid  10138  fseq1p1m1  10374  nn0split  10416  nnsplit  10417  fzosplitsnm1  10500  fzosplitpr  10525  fzosplitprm1  10526  ceilid  10623  flqdiv  10629  zmod10  10648  modqcyc  10667  modqaddabs  10670  mulqaddmodid  10672  modqadd2mod  10682  modqm1p1mod0  10683  modqmul12d  10686  modqadd12d  10688  modqmulmodr  10698  modqaddmulmod  10699  frecuzrdgsuc  10722  seqeq123d  10764  seqvalcd  10769  seq3f1olemqsumkj  10819  seq3f1oleml  10824  seqf1oglem2  10828  seq3id3  10832  seq3id  10833  seq3homo  10835  seq3z  10836  seqhomog  10838  exp1  10853  expnegap0  10855  expmulzap  10893  m1expeven  10894  expdivap  10898  binom3  10965  sqoddm1div8  11001  mulsubdivbinom2ap  11019  bcn1  11066  bcnp1n  11067  bcval5  11071  bcn2m1  11077  bcn2p1  11078  hashdifpr  11130  ccatlen  11221  ccatalpha  11239  ccatw2s1leng  11264  ccats1val2  11266  lswccats1  11269  swrdlend  11288  ccatswrd  11300  pfxmpt  11310  pfxfv  11314  pfxfvlsw  11325  ccatpfx  11331  pfx1  11333  pfxswrd  11336  swrdpfx  11337  pfxpfx  11338  lenrevpfxcctswrd  11342  wrdind  11352  wrd2ind  11353  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatpfx2  11367  pfxccatid  11371  cats1fvnd  11395  crim  11481  remullem  11494  remul2  11496  immul2  11503  ipcnval  11509  cjreim  11526  recvguniqlem  11617  resqrexlemover  11633  resqrexlemcalc1  11637  absid  11694  amgm2  11741  max0addsup  11842  minabs  11859  xrmaxrecl  11878  xrminadd  11898  fsumsplitf  12032  sumsnf  12033  fsump1i  12057  fsum2dlemstep  12058  fsumshftm  12069  fsummulc2  12072  modfsummodlemstep  12081  telfsumo  12090  fsumrelem  12095  hash2iun1dif1  12104  binomlem  12107  binom1dif  12111  arisum  12122  geo2sum  12138  geo2sum2  12139  cvgratz  12156  mertenslemi1  12159  clim2prod  12163  fprodeq0  12241  fprod2dlemstep  12246  fproddivap  12254  fproddivapf  12255  fprodmodd  12265  ef0lem  12284  eftlub  12314  efsep  12315  effsumlt  12316  tanval2ap  12337  efi4p  12341  resin4p  12342  recos4p  12343  efeul  12358  sinadd  12360  cosadd  12361  sinmul  12368  ef01bndlem  12380  cos12dec  12392  absef  12394  demoivreALT  12398  dvds2ln  12448  dvdseq  12472  opeo  12521  bezoutlemnewy  12630  nninfctlemfo  12674  eucalginv  12691  eucalglt  12692  eucalg  12694  lcmgcdlem  12712  lcm1  12716  divgcdcoprmex  12737  2sqpwodd  12811  zgcdsq  12836  qden1elz  12840  phiprmpw  12857  eulerthlem1  12862  eulerthlemrprm  12864  prmdiv  12870  hashgcdlem  12873  odzdvds  12881  vfermltl  12887  modprm0  12890  pythagtriplem12  12911  pcqmul  12939  pcaddlem  12975  pcadd  12976  pcadd2  12977  pcmpt  12979  pcmpt2  12980  mul4sqlem  13029  4sqlem11  13037  4sqlem17  13043  nninfdclemp1  13134  ressressg  13221  gsumsplit1r  13544  gsumprval  13545  mndinvmod  13591  mhmco  13636  gsumfzz  13641  grpinvid2  13699  grpasscan2  13710  grpinvssd  13723  grpinvadd  13724  grpsubid1  13731  grpsubadd  13734  grppncan  13737  mulg1  13779  mulgaddcomlem  13795  mulgdirlem  13803  mulgneg2  13806  mulgmodid  13811  nmzsubg  13860  qusinv  13886  qussub  13887  conjnmz  13929  ablsub2inv  13961  abladdsub4  13964  abladdsub  13965  ablpncan2  13966  ablpnpcan  13970  ablnncan  13971  invghm  13979  gsumfzconst  13991  gsumfzsnfd  13995  rngm2neg  14026  srgpcompp  14068  srgpcomppsc  14069  ringinvnzdiv  14127  ringm2neg  14132  dvr1  14216  dvrcan1  14218  dvrcan3  14219  rdivmuldivd  14222  lmodfopne  14405  sralemg  14517  gsumfzfsumlemm  14666  mplsubgfilemcl  14783  mplsubgfileminv  14784  xmetxpbl  15302  ivthinclemuopn  15432  limcimolemlt  15458  cnplimcim  15461  limccnpcntop  15469  limccnp2lem  15470  dvexp  15505  dvmptcmulcn  15515  dvply1  15559  ef2kpi  15600  sinhalfpip  15614  sinhalfpim  15615  coshalfpim  15617  ptolemy  15618  tangtx  15632  rpabscxpbnd  15734  relogbexpap  15752  rplogbcxp  15757  rpcxplogb  15758  binom4  15773  pellexlem2  15775  wilthlem1  15777  0sgm  15782  mpodvdsmulf1o  15787  fsumdvdsmul  15788  sgmppw  15789  0sgmppw  15790  1sgm2ppw  15792  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsval2lem  15812  lgsval4  15822  lgsval4a  15824  lgsneg  15826  lgsneg1  15827  lgsdirprm  15836  lgsdir  15837  lgsne0  15840  lgsmulsqcoprm  15848  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  gausslemma2d  15871  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem1  15883  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2sqlem3  15919  structiedg0val  15964  uhgr2edg  16130  usgr1e  16165  vtxdgfifival  16215  vtxdfifiun  16221  vtxdumgrfival  16222  vtxduspgrfvedgfi  16225  1loopgredg  16228  1loopgrvd2fi  16229  1hevtxdg1en  16232  p1evtxdeqfi  16236  edginwlkd  16279  clwwlknonex2lem1  16361  eupthvdres  16399  peano4nninf  16715  repiecele0  16741  repiecege0  16742  trilpolemclim  16751  trilpolemeq1  16755  apdifflemf  16761  gfsumval  16792  gfsumsn  16797