Theorem 3eqtrd 2174

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

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  tpeq123d  3610  diftpsn3  3656  oteq123d  3715  resiima  4892  fvun1  5480  fvmptd  5495  fmptpr  5605  caovlem2d  5956  offval  5982  ofvalg  5984  cnvf1olem  6114  nnm1  6413  updjudhcoinlf  6958  updjudhcoinrg  6959  caseinl  6969  caseinr  6970  omp1eomlem  6972  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  ltexnqq  7209  prarloclemarch  7219  ltrnqg  7221  nq02m  7266  prarloclemcalc  7303  mulnqprl  7369  mulnqpru  7370  ltexprlemloc  7408  addcanprleml  7415  recexprlem1ssu  7435  cauappcvgprlem1  7460  caucvgsrlemfv  7592  caucvgsrlemoffval  7597  recidpirqlemcalc  7658  axmulass  7674  axrnegex  7680  muladd11r  7911  addcan2  7936  addsub  7966  subsub2  7983  negsubdi2  8014  muladd  8139  mulsub  8156  cru  8357  mulreim  8359  recextlem1  8405  mulap0  8408  muleqadd  8422  divrecap  8441  div23ap  8444  div12ap  8447  divmulasscomap  8449  divcanap7  8474  conjmulap  8482  apmul1  8541  nndivtr  8755  xp1d2m1eqxm1d2  8965  div4p1lem1div2  8966  qapne  9424  xnegneg  9609  rexsub  9629  xnegid  9635  fseq1p1m1  9867  nn0split  9906  nnsplit  9907  fzosplitsnm1  9979  fzosplitprm1  10004  ceilid  10081  flqdiv  10087  zmod10  10106  modqcyc  10125  modqaddabs  10128  mulqaddmodid  10130  modqadd2mod  10140  modqm1p1mod0  10141  modqmul12d  10144  modqadd12d  10146  modqmulmodr  10156  modqaddmulmod  10157  frecuzrdgsuc  10180  seqeq123d  10220  seqvalcd  10225  seq3f1olemqsumkj  10264  seq3f1oleml  10269  seq3id3  10273  seq3id  10274  seq3homo  10276  seq3z  10277  exp1  10292  expnegap0  10294  expmulzap  10332  m1expeven  10333  expdivap  10337  binom3  10402  sqoddm1div8  10437  bcn1  10497  bcnp1n  10498  bcval5  10502  bcn2m1  10508  bcn2p1  10509  hashdifpr  10559  crim  10623  remullem  10636  remul2  10638  immul2  10645  ipcnval  10651  cjreim  10668  recvguniqlem  10759  resqrexlemover  10775  resqrexlemcalc1  10779  absid  10836  amgm2  10883  max0addsup  10984  minabs  11000  xrmaxrecl  11017  xrminadd  11037  fsumsplitf  11170  sumsnf  11171  fsump1i  11195  fsum2dlemstep  11196  fsumshftm  11207  fsummulc2  11210  modfsummodlemstep  11219  telfsumo  11228  fsumrelem  11233  hash2iun1dif1  11242  binomlem  11245  binom1dif  11249  arisum  11260  geo2sum  11276  geo2sum2  11277  cvgratz  11294  mertenslemi1  11297  clim2prod  11301  ef0lem  11355  eftlub  11385  efsep  11386  effsumlt  11387  tanval2ap  11409  efi4p  11413  resin4p  11414  recos4p  11415  efeul  11430  sinadd  11432  cosadd  11433  sinmul  11440  ef01bndlem  11452  cos12dec  11463  absef  11465  demoivreALT  11469  dvds2ln  11515  dvdseq  11535  opeo  11583  bezoutlemnewy  11673  eucalginv  11726  eucalglt  11727  eucalg  11729  lcmgcdlem  11747  lcm1  11751  divgcdcoprmex  11772  2sqpwodd  11843  zgcdsq  11868  qden1elz  11872  phiprmpw  11887  hashgcdlem  11892  xmetxpbl  12666  ivthinclemuopn  12774  limcimolemlt  12791  cnplimcim  12794  limccnpcntop  12802  limccnp2lem  12803  dvexp  12833  dvmptcmulcn  12841  ef2kpi  12876  sinhalfpip  12890  sinhalfpim  12891  coshalfpim  12893  ptolemy  12894  tangtx  12908  peano4nninf  13189  trilpolemclim  13218  trilpolemeq1  13222