Theorem 3eqtrd 2076

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

Syntax hints:   → wi 4   = wceq 1243

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  tpeq123d  3462  diftpsn3  3505  oteq123d  3564  resiima  4683  fvun1  5239  fvmptd  5253  fmptpr  5355  caovlem2d  5693  offval  5719  fnofval  5721  cnvf1olem  5845  nnm1  6097  ltexnqq  6506  prarloclemarch  6516  ltrnqg  6518  nq02m  6563  prarloclemcalc  6600  mulnqprl  6666  mulnqpru  6667  ltexprlemloc  6705  addcanprleml  6712  recexprlem1ssu  6732  cauappcvgprlem1  6757  caucvgsrlemfv  6875  caucvgsrlemoffval  6880  recidpirqlemcalc  6933  axmulass  6947  axrnegex  6953  addcan2  7192  addsub  7222  subsub2  7239  negsubdi2  7270  muladd  7381  mulsub  7398  cru  7593  mulreim  7595  recextlem1  7632  mulap0  7635  muleqadd  7649  divrecap  7667  div23ap  7670  div12ap  7673  divcanap7  7697  conjmulap  7705  apmul1  7764  nndivtr  7955  div4p1lem1div2  8177  qapne  8574  xnegneg  8746  fseq1p1m1  8956  nn0split  8994  fzosplitsnm1  9065  fzosplitprm1  9090  ceilid  9157  flqdiv  9163  zmod10  9182  frecuzrdgsuc  9201  iseqid3s  9246  iseqid  9247  iseqhomo  9248  exp1  9261  expnegap0  9263  expmulzap  9301  expdivap  9305  binom3  9366  crim  9458  remullem  9471  remul2  9473  immul2  9480  ipcnval  9486  cjreim  9503  recvguniqlem  9592  resqrexlemover  9608  resqrexlemcalc1  9612  absid  9669  amgm2  9714