Theorem 3eqtrd 2214

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  tpeq123d  3684  diftpsn3  3733  oteq123d  3793  resiima  4986  fvun1  5582  fvmptd  5597  fmptpr  5708  caovlem2d  6066  offval  6089  ofvalg  6091  cnvf1olem  6224  nnm1  6525  updjudhcoinlf  7078  updjudhcoinrg  7079  caseinl  7089  caseinr  7090  omp1eomlem  7092  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  ltexnqq  7406  prarloclemarch  7416  ltrnqg  7418  nq02m  7463  prarloclemcalc  7500  mulnqprl  7566  mulnqpru  7567  ltexprlemloc  7605  addcanprleml  7612  recexprlem1ssu  7632  cauappcvgprlem1  7657  caucvgsrlemfv  7789  caucvgsrlemoffval  7794  recidpirqlemcalc  7855  axmulass  7871  axrnegex  7877  muladd11r  8112  addcan2  8137  addsub  8167  subsub2  8184  negsubdi2  8215  muladd  8340  mulsub  8357  cru  8558  mulreim  8560  recextlem1  8607  mulap0  8610  muleqadd  8624  divrecap  8644  div23ap  8647  div12ap  8650  divmulasscomap  8652  divcanap7  8677  conjmulap  8685  apmul1  8744  nndivtr  8960  xp1d2m1eqxm1d2  9170  div4p1lem1div2  9171  qapne  9638  xnegneg  9832  rexsub  9852  xnegid  9858  fseq1p1m1  10093  nn0split  10135  nnsplit  10136  fzosplitsnm1  10208  fzosplitprm1  10233  ceilid  10314  flqdiv  10320  zmod10  10339  modqcyc  10358  modqaddabs  10361  mulqaddmodid  10363  modqadd2mod  10373  modqm1p1mod0  10374  modqmul12d  10377  modqadd12d  10379  modqmulmodr  10389  modqaddmulmod  10390  frecuzrdgsuc  10413  seqeq123d  10453  seqvalcd  10458  seq3f1olemqsumkj  10497  seq3f1oleml  10502  seq3id3  10506  seq3id  10507  seq3homo  10509  seq3z  10510  exp1  10525  expnegap0  10527  expmulzap  10565  m1expeven  10566  expdivap  10570  binom3  10637  sqoddm1div8  10673  mulsubdivbinom2ap  10690  bcn1  10737  bcnp1n  10738  bcval5  10742  bcn2m1  10748  bcn2p1  10749  hashdifpr  10799  crim  10866  remullem  10879  remul2  10881  immul2  10888  ipcnval  10894  cjreim  10911  recvguniqlem  11002  resqrexlemover  11018  resqrexlemcalc1  11022  absid  11079  amgm2  11126  max0addsup  11227  minabs  11243  xrmaxrecl  11262  xrminadd  11282  fsumsplitf  11415  sumsnf  11416  fsump1i  11440  fsum2dlemstep  11441  fsumshftm  11452  fsummulc2  11455  modfsummodlemstep  11464  telfsumo  11473  fsumrelem  11478  hash2iun1dif1  11487  binomlem  11490  binom1dif  11494  arisum  11505  geo2sum  11521  geo2sum2  11522  cvgratz  11539  mertenslemi1  11542  clim2prod  11546  fprodeq0  11624  fprod2dlemstep  11629  fproddivap  11637  fproddivapf  11638  fprodmodd  11648  ef0lem  11667  eftlub  11697  efsep  11698  effsumlt  11699  tanval2ap  11720  efi4p  11724  resin4p  11725  recos4p  11726  efeul  11741  sinadd  11743  cosadd  11744  sinmul  11751  ef01bndlem  11763  cos12dec  11774  absef  11776  demoivreALT  11780  dvds2ln  11830  dvdseq  11853  opeo  11901  bezoutlemnewy  11996  eucalginv  12055  eucalglt  12056  eucalg  12058  lcmgcdlem  12076  lcm1  12080  divgcdcoprmex  12101  2sqpwodd  12175  zgcdsq  12200  qden1elz  12204  phiprmpw  12221  eulerthlem1  12226  eulerthlemrprm  12228  prmdiv  12234  hashgcdlem  12237  odzdvds  12244  vfermltl  12250  modprm0  12253  pythagtriplem12  12274  pcqmul  12302  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmpt2  12341  mul4sqlem  12390  nninfdclemp1  12450  ressressg  12533  mndinvmod  12845  mhmco  12873  grpinvid2  12924  grpasscan2  12933  grpinvssd  12946  grpinvadd  12947  grpsubid1  12954  grpsubadd  12957  grppncan  12960  mulg1  12989  mulgaddcomlem  13004  mulgdirlem  13012  mulgneg2  13015  mulgmodid  13020  nmzsubg  13068  ablsub2inv  13112  abladdsub4  13115  abladdsub  13116  ablpncan2  13117  ablpnpcan  13121  ablnncan  13122  srgpcompp  13172  srgpcomppsc  13173  ringinvnzdiv  13225  ringm2neg  13230  dvr1  13305  dvrcan1  13307  dvrcan3  13308  rdivmuldivd  13311  xmetxpbl  13978  ivthinclemuopn  14086  limcimolemlt  14103  cnplimcim  14106  limccnpcntop  14114  limccnp2lem  14115  dvexp  14145  dvmptcmulcn  14153  ef2kpi  14197  sinhalfpip  14211  sinhalfpim  14212  coshalfpim  14214  ptolemy  14215  tangtx  14229  rpabscxpbnd  14329  relogbexpap  14346  rplogbcxp  14351  rpcxplogb  14352  binom4  14367  lgsval2lem  14381  lgsval4  14391  lgsval4a  14393  lgsneg  14395  lgsneg1  14396  lgsdirprm  14405  lgsdir  14406  lgsne0  14409  lgsmulsqcoprm  14417  2sqlem3  14434  peano4nninf  14725  trilpolemclim  14754  trilpolemeq1  14758  apdifflemf  14764