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  6448  prarloclemcalc  6485  mulnqprl  6549  mulnqpru  6550  ltexprlemloc  6581  addcanprleml  6588  recexprlem1ssu  6606  cauappcvgprlem1  6631  axmulass  6757  axrnegex  6763  addcan2  6989  addsub  7019  subsub2  7035  negsubdi2  7066  muladd  7177  mulsub  7194  cru  7386  mulreim  7388  recextlem1  7414  mulap0  7417  muleqadd  7431  divrecap  7449  div23ap  7452  div12ap  7455  divcanap7  7479  conjmulap  7487  apmul1  7546  nndivtr  7736  qapne  8350  xnegneg  8516  fseq1p1m1  8726  nn0split  8764  fzosplitsnm1  8835  fzosplitprm1  8860  frecuzrdgsuc  8882  exp1  8915  expnegap0  8917  expmulzap  8955  expdivap  8959  binom3  9019  crim  9086  remullem  9099  remul2  9101  immul2  9108  ipcnval  9114  cjreim  9131  absid  9225