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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fmptapd  5845  rdgisucinc  6551  ctm  7308  mulidnq  7609  ltrnqg  7640  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  mulcmpblnrlemg  7960  caucvgsrlemoffcau  8018  negsub  8427  neg2sub  8439  divmuleqap  8897  divneg2ap  8916  qapne  9873  seqvalcd  10724  binom2  10914  bcpasc  11029  cats2catd  11354  crim  11423  remullem  11436  max0addsup  11784  summodclem2a  11947  isum1p  12058  geo2sum  12080  cvgratz  12098  efi4p  12283  tanaddap  12305  addcos  12312  cos2tsin  12317  demoivreALT  12340  omeo  12464  sqgcd  12605  eulerthlemth  12809  pythagtriplem16  12857  fldivp1  12926  pockthlem  12934  4sqlem10  12965  gsumval2  13485  grpinvid2  13641  imasgrp2  13702  mulgaddcomlem  13737  mulgmodid  13753  ablsubsub  13910  ablsubsub4  13911  gsumfzsnfd  13937  opprunitd  14130  lmodfopne  14346  mpl0fi  14722  mplnegfi  14725  txrest  15006  limccnpcntop  15405  dvrecap  15443  dvply1  15495  cosq34lt1  15580  wilthlem1  15710  mersenne  15727  lgseisenlem1  15805  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  2lgslem1  15826  qdiff  16679