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  5834  rdgisucinc  6537  ctm  7287  mulidnq  7587  ltrnqg  7618  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  mulcmpblnrlemg  7938  caucvgsrlemoffcau  7996  negsub  8405  neg2sub  8417  divmuleqap  8875  divneg2ap  8894  qapne  9846  seqvalcd  10695  binom2  10885  bcpasc  11000  cats2catd  11316  crim  11384  remullem  11397  max0addsup  11745  summodclem2a  11907  isum1p  12018  geo2sum  12040  cvgratz  12058  efi4p  12243  tanaddap  12265  addcos  12272  cos2tsin  12277  demoivreALT  12300  omeo  12424  sqgcd  12565  eulerthlemth  12769  pythagtriplem16  12817  fldivp1  12886  pockthlem  12894  4sqlem10  12925  gsumval2  13445  grpinvid2  13601  imasgrp2  13662  mulgaddcomlem  13697  mulgmodid  13713  ablsubsub  13870  ablsubsub4  13871  gsumfzsnfd  13897  opprunitd  14089  lmodfopne  14305  mpl0fi  14681  mplnegfi  14684  txrest  14965  limccnpcntop  15364  dvrecap  15402  dvply1  15454  cosq34lt1  15539  wilthlem1  15669  mersenne  15686  lgseisenlem1  15764  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  2lgslem1  15785