Theorem 3eqtr2d 2271

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

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

This theorem is referenced by:  fmptapd  5875  rdgisucinc  6616  ctm  7400  mulidnq  7704  ltrnqg  7735  recexprlem1ssl  7948  recexprlem1ssu  7949  ltmprr  7957  mulcmpblnrlemg  8055  caucvgsrlemoffcau  8113  negsub  8521  neg2sub  8533  divmuleqap  8991  divneg2ap  9010  qapne  9971  seqvalcd  10823  binom2  11013  bcpasc  11128  cats2catd  11461  crim  11543  remullem  11556  max0addsup  11904  summodclem2a  12067  isum1p  12178  geo2sum  12200  cvgratz  12218  efi4p  12403  tanaddap  12425  addcos  12432  cos2tsin  12437  demoivreALT  12460  omeo  12584  sqgcd  12725  eulerthlemth  12929  pythagtriplem16  12977  fldivp1  13046  pockthlem  13054  4sqlem10  13085  gsumval2  13610  grpinvid2  13766  imasgrp2  13827  mulgaddcomlem  13862  mulgmodid  13878  ablsubsub  14035  ablsubsub4  14036  gsumfzsnfd  14062  opprunitd  14255  lmodfopne  14474  mpl0fi  14857  mplnegfi  14860  txrest  15141  limccnpcntop  15540  dvrecap  15578  dvply1  15630  cosq34lt1  15715  wilthlem1  15848  mersenne  15865  lgseisenlem1  15943  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  2lgslem1  15964  qdiff  16833