Theorem 3eqtr2d 2270

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2d	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2267	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2264	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  fmptapd  5853  rdgisucinc  6594  ctm  7351  mulidnq  7652  ltrnqg  7683  recexprlem1ssl  7896  recexprlem1ssu  7897  ltmprr  7905  mulcmpblnrlemg  8003  caucvgsrlemoffcau  8061  negsub  8469  neg2sub  8481  divmuleqap  8939  divneg2ap  8958  qapne  9917  seqvalcd  10769  binom2  10959  bcpasc  11074  cats2catd  11399  crim  11481  remullem  11494  max0addsup  11842  summodclem2a  12005  isum1p  12116  geo2sum  12138  cvgratz  12156  efi4p  12341  tanaddap  12363  addcos  12370  cos2tsin  12375  demoivreALT  12398  omeo  12522  sqgcd  12663  eulerthlemth  12867  pythagtriplem16  12915  fldivp1  12984  pockthlem  12992  4sqlem10  13023  gsumval2  13543  grpinvid2  13699  imasgrp2  13760  mulgaddcomlem  13795  mulgmodid  13811  ablsubsub  13968  ablsubsub4  13969  gsumfzsnfd  13995  opprunitd  14188  lmodfopne  14405  mpl0fi  14786  mplnegfi  14789  txrest  15070  limccnpcntop  15469  dvrecap  15507  dvply1  15559  cosq34lt1  15644  wilthlem1  15777  mersenne  15794  lgseisenlem1  15872  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  2lgslem1  15893  qdiff  16764