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  3685  diftpsn3  3734  oteq123d  3794  resiima  4987  fvun1  5583  fvmptd  5598  fmptpr  5709  caovlem2d  6067  offval  6090  ofvalg  6092  cnvf1olem  6225  nnm1  6526  updjudhcoinlf  7079  updjudhcoinrg  7080  caseinl  7090  caseinr  7091  omp1eomlem  7093  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  ltexnqq  7407  prarloclemarch  7417  ltrnqg  7419  nq02m  7464  prarloclemcalc  7501  mulnqprl  7567  mulnqpru  7568  ltexprlemloc  7606  addcanprleml  7613  recexprlem1ssu  7633  cauappcvgprlem1  7658  caucvgsrlemfv  7790  caucvgsrlemoffval  7795  recidpirqlemcalc  7856  axmulass  7872  axrnegex  7878  muladd11r  8113  addcan2  8138  addsub  8168  subsub2  8185  negsubdi2  8216  muladd  8341  mulsub  8358  cru  8559  mulreim  8561  recextlem1  8608  mulap0  8611  muleqadd  8625  divrecap  8645  div23ap  8648  div12ap  8651  divmulasscomap  8653  divcanap7  8678  conjmulap  8686  apmul1  8745  nndivtr  8961  xp1d2m1eqxm1d2  9171  div4p1lem1div2  9172  qapne  9639  xnegneg  9833  rexsub  9853  xnegid  9859  fseq1p1m1  10094  nn0split  10136  nnsplit  10137  fzosplitsnm1  10209  fzosplitprm1  10234  ceilid  10315  flqdiv  10321  zmod10  10340  modqcyc  10359  modqaddabs  10362  mulqaddmodid  10364  modqadd2mod  10374  modqm1p1mod0  10375  modqmul12d  10378  modqadd12d  10380  modqmulmodr  10390  modqaddmulmod  10391  frecuzrdgsuc  10414  seqeq123d  10454  seqvalcd  10459  seq3f1olemqsumkj  10498  seq3f1oleml  10503  seq3id3  10507  seq3id  10508  seq3homo  10510  seq3z  10511  exp1  10526  expnegap0  10528  expmulzap  10566  m1expeven  10567  expdivap  10571  binom3  10638  sqoddm1div8  10674  mulsubdivbinom2ap  10691  bcn1  10738  bcnp1n  10739  bcval5  10743  bcn2m1  10749  bcn2p1  10750  hashdifpr  10800  crim  10867  remullem  10880  remul2  10882  immul2  10889  ipcnval  10895  cjreim  10912  recvguniqlem  11003  resqrexlemover  11019  resqrexlemcalc1  11023  absid  11080  amgm2  11127  max0addsup  11228  minabs  11244  xrmaxrecl  11263  xrminadd  11283  fsumsplitf  11416  sumsnf  11417  fsump1i  11441  fsum2dlemstep  11442  fsumshftm  11453  fsummulc2  11456  modfsummodlemstep  11465  telfsumo  11474  fsumrelem  11479  hash2iun1dif1  11488  binomlem  11491  binom1dif  11495  arisum  11506  geo2sum  11522  geo2sum2  11523  cvgratz  11540  mertenslemi1  11543  clim2prod  11547  fprodeq0  11625  fprod2dlemstep  11630  fproddivap  11638  fproddivapf  11639  fprodmodd  11649  ef0lem  11668  eftlub  11698  efsep  11699  effsumlt  11700  tanval2ap  11721  efi4p  11725  resin4p  11726  recos4p  11727  efeul  11742  sinadd  11744  cosadd  11745  sinmul  11752  ef01bndlem  11764  cos12dec  11775  absef  11777  demoivreALT  11781  dvds2ln  11831  dvdseq  11854  opeo  11902  bezoutlemnewy  11997  eucalginv  12056  eucalglt  12057  eucalg  12059  lcmgcdlem  12077  lcm1  12081  divgcdcoprmex  12102  2sqpwodd  12176  zgcdsq  12201  qden1elz  12205  phiprmpw  12222  eulerthlem1  12227  eulerthlemrprm  12229  prmdiv  12235  hashgcdlem  12238  odzdvds  12245  vfermltl  12251  modprm0  12254  pythagtriplem12  12275  pcqmul  12303  pcaddlem  12338  pcadd  12339  pcmpt  12341  pcmpt2  12342  mul4sqlem  12391  nninfdclemp1  12451  ressressg  12534  mndinvmod  12846  mhmco  12874  grpinvid2  12925  grpasscan2  12934  grpinvssd  12947  grpinvadd  12948  grpsubid1  12955  grpsubadd  12958  grppncan  12961  mulg1  12990  mulgaddcomlem  13006  mulgdirlem  13014  mulgneg2  13017  mulgmodid  13022  nmzsubg  13070  ablsub2inv  13114  abladdsub4  13117  abladdsub  13118  ablpncan2  13119  ablpnpcan  13123  ablnncan  13124  srgpcompp  13174  srgpcomppsc  13175  ringinvnzdiv  13227  ringm2neg  13232  dvr1  13307  dvrcan1  13309  dvrcan3  13310  rdivmuldivd  13313  lmodfopne  13416  xmetxpbl  14011  ivthinclemuopn  14119  limcimolemlt  14136  cnplimcim  14139  limccnpcntop  14147  limccnp2lem  14148  dvexp  14178  dvmptcmulcn  14186  ef2kpi  14230  sinhalfpip  14244  sinhalfpim  14245  coshalfpim  14247  ptolemy  14248  tangtx  14262  rpabscxpbnd  14362  relogbexpap  14379  rplogbcxp  14384  rpcxplogb  14385  binom4  14400  lgsval2lem  14414  lgsval4  14424  lgsval4a  14426  lgsneg  14428  lgsneg1  14429  lgsdirprm  14438  lgsdir  14439  lgsne0  14442  lgsmulsqcoprm  14450  2sqlem3  14467  peano4nninf  14758  trilpolemclim  14787  trilpolemeq1  14791  apdifflemf  14797