Theorem 3eqtr2d 2268

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 2265	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2262	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fmptapd  5840  rdgisucinc  6546  ctm  7299  mulidnq  7599  ltrnqg  7630  recexprlem1ssl  7843  recexprlem1ssu  7844  ltmprr  7852  mulcmpblnrlemg  7950  caucvgsrlemoffcau  8008  negsub  8417  neg2sub  8429  divmuleqap  8887  divneg2ap  8906  qapne  9863  seqvalcd  10713  binom2  10903  bcpasc  11018  cats2catd  11340  crim  11409  remullem  11422  max0addsup  11770  summodclem2a  11932  isum1p  12043  geo2sum  12065  cvgratz  12083  efi4p  12268  tanaddap  12290  addcos  12297  cos2tsin  12302  demoivreALT  12325  omeo  12449  sqgcd  12590  eulerthlemth  12794  pythagtriplem16  12842  fldivp1  12911  pockthlem  12919  4sqlem10  12950  gsumval2  13470  grpinvid2  13626  imasgrp2  13687  mulgaddcomlem  13722  mulgmodid  13738  ablsubsub  13895  ablsubsub4  13896  gsumfzsnfd  13922  opprunitd  14114  lmodfopne  14330  mpl0fi  14706  mplnegfi  14709  txrest  14990  limccnpcntop  15389  dvrecap  15427  dvply1  15479  cosq34lt1  15564  wilthlem1  15694  mersenne  15711  lgseisenlem1  15789  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  2lgslem1  15810