Theorem 3eqtrd 2151

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

Syntax hints:   → wi 4   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  tpeq123d  3581  diftpsn3  3627  oteq123d  3686  resiima  4855  fvun1  5441  fvmptd  5456  fmptpr  5566  caovlem2d  5917  offval  5943  ofvalg  5945  cnvf1olem  6075  nnm1  6374  updjudhcoinlf  6917  updjudhcoinrg  6918  caseinl  6928  caseinr  6929  omp1eomlem  6931  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  ltexnqq  7164  prarloclemarch  7174  ltrnqg  7176  nq02m  7221  prarloclemcalc  7258  mulnqprl  7324  mulnqpru  7325  ltexprlemloc  7363  addcanprleml  7370  recexprlem1ssu  7390  cauappcvgprlem1  7415  caucvgsrlemfv  7533  caucvgsrlemoffval  7538  recidpirqlemcalc  7592  axmulass  7608  axrnegex  7614  muladd11r  7841  addcan2  7866  addsub  7896  subsub2  7913  negsubdi2  7944  muladd  8065  mulsub  8082  cru  8282  mulreim  8284  recextlem1  8325  mulap0  8328  muleqadd  8342  divrecap  8361  div23ap  8364  div12ap  8367  divmulasscomap  8369  divcanap7  8394  conjmulap  8402  apmul1  8461  nndivtr  8672  xp1d2m1eqxm1d2  8876  div4p1lem1div2  8877  qapne  9333  xnegneg  9509  rexsub  9529  xnegid  9535  fseq1p1m1  9767  nn0split  9806  nnsplit  9807  fzosplitsnm1  9879  fzosplitprm1  9904  ceilid  9981  flqdiv  9987  zmod10  10006  modqcyc  10025  modqaddabs  10028  mulqaddmodid  10030  modqadd2mod  10040  modqm1p1mod0  10041  modqmul12d  10044  modqadd12d  10046  modqmulmodr  10056  modqaddmulmod  10057  frecuzrdgsuc  10080  seqeq123d  10120  seqvalcd  10125  seq3f1olemqsumkj  10164  seq3f1oleml  10169  seq3id3  10173  seq3id  10174  seq3homo  10176  seq3z  10177  exp1  10192  expnegap0  10194  expmulzap  10232  m1expeven  10233  expdivap  10237  binom3  10302  sqoddm1div8  10337  bcn1  10397  bcnp1n  10398  bcval5  10402  bcn2m1  10408  bcn2p1  10409  hashdifpr  10459  crim  10523  remullem  10536  remul2  10538  immul2  10545  ipcnval  10551  cjreim  10568  recvguniqlem  10658  resqrexlemover  10674  resqrexlemcalc1  10678  absid  10735  amgm2  10782  max0addsup  10883  minabs  10899  xrmaxrecl  10916  xrminadd  10936  fsumsplitf  11069  sumsnf  11070  fsump1i  11094  fsum2dlemstep  11095  fsumshftm  11106  fsummulc2  11109  modfsummodlemstep  11118  telfsumo  11127  fsumrelem  11132  hash2iun1dif1  11141  binomlem  11144  binom1dif  11148  arisum  11159  geo2sum  11175  geo2sum2  11176  cvgratz  11193  mertenslemi1  11196  ef0lem  11217  eftlub  11247  efsep  11248  effsumlt  11249  tanval2ap  11271  efi4p  11275  resin4p  11276  recos4p  11277  efeul  11292  sinadd  11294  cosadd  11295  sinmul  11302  ef01bndlem  11314  absef  11326  demoivreALT  11330  dvds2ln  11374  dvdseq  11394  opeo  11442  bezoutlemnewy  11530  eucalginv  11583  eucalglt  11584  eucalg  11586  lcmgcdlem  11604  lcm1  11608  divgcdcoprmex  11629  2sqpwodd  11699  zgcdsq  11724  qden1elz  11728  phiprmpw  11743  hashgcdlem  11748  xmetxpbl  12497  limcimolemlt  12589  cnplimcim  12592  limccnpcntop  12600  limccnp2lem  12601  peano4nninf  12890  trilpolemclim  12919  trilpolemeq1  12923