Theorem 3eqtrd 2073

Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (φ → A = B)
3eqtrd.2	⊢ (φ → B = 𝐶)
3eqtrd.3	⊢ (φ → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtrd	⊢ (φ → A = 𝐷)

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 ⊢ (φ → A = B)
2		3eqtrd.2	. . 3 ⊢ (φ → B = 𝐶)
3		3eqtrd.3	. . 3 ⊢ (φ → 𝐶 = 𝐷)
4	2, 3	eqtrd 2069	. 2 ⊢ (φ → B = 𝐷)
5	1, 4	eqtrd 2069	1 ⊢ (φ → A = 𝐷)

Syntax hints:   → wi 4   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  tpeq123d  3453  diftpsn3  3496  oteq123d  3555  resiima  4626  fvun1  5182  fvmptd  5196  fmptpr  5298  caovlem2d  5635  offval  5661  fnofval  5663  cnvf1olem  5787  nnm1  6033  ltexnqq  6391  prarloclemarch  6401  ltrnqg  6403  nq02m  6447  prarloclemcalc  6484  mulnqprl  6547  mulnqpru  6548  ltexprlemloc  6579  addcanprleml  6586  recexprlem1ssu  6604  axmulass  6717  axrnegex  6723  addcan2  6949  addsub  6979  subsub2  6995  negsubdi2  7026  muladd  7137  mulsub  7154  cru  7346  mulreim  7348  recextlem1  7374  mulap0  7377  muleqadd  7391  divrecap  7409  div23ap  7412  div12ap  7415  divcanap7  7439  conjmulap  7447  apmul1  7506  nndivtr  7696  qapne  8310  xnegneg  8476  fseq1p1m1  8686  nn0split  8724  fzosplitsnm1  8795  fzosplitprm1  8820  frecuzrdgsuc  8842  exp1  8875  expnegap0  8877  expmulzap  8915  expdivap  8919  binom3  8979  crim  9046  remullem  9059  remul2  9061  immul2  9068  ipcnval  9074  cjreim  9091