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  5829  rdgisucinc  6529  ctm  7272  mulidnq  7572  ltrnqg  7603  recexprlem1ssl  7816  recexprlem1ssu  7817  ltmprr  7825  mulcmpblnrlemg  7923  caucvgsrlemoffcau  7981  negsub  8390  neg2sub  8402  divmuleqap  8860  divneg2ap  8879  qapne  9830  seqvalcd  10678  binom2  10868  bcpasc  10983  cats2catd  11296  crim  11364  remullem  11377  max0addsup  11725  summodclem2a  11887  isum1p  11998  geo2sum  12020  cvgratz  12038  efi4p  12223  tanaddap  12245  addcos  12252  cos2tsin  12257  demoivreALT  12280  omeo  12404  sqgcd  12545  eulerthlemth  12749  pythagtriplem16  12797  fldivp1  12866  pockthlem  12874  4sqlem10  12905  gsumval2  13425  grpinvid2  13581  imasgrp2  13642  mulgaddcomlem  13677  mulgmodid  13693  ablsubsub  13850  ablsubsub4  13851  gsumfzsnfd  13877  opprunitd  14068  lmodfopne  14284  mpl0fi  14660  mplnegfi  14663  txrest  14944  limccnpcntop  15343  dvrecap  15381  dvply1  15433  cosq34lt1  15518  wilthlem1  15648  mersenne  15665  lgseisenlem1  15743  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem1  15754  2lgslem1  15764