Theorem 3eqtr2d 2245

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  fmptapd  5787  rdgisucinc  6483  ctm  7225  mulidnq  7517  ltrnqg  7548  recexprlem1ssl  7761  recexprlem1ssu  7762  ltmprr  7770  mulcmpblnrlemg  7868  caucvgsrlemoffcau  7926  negsub  8335  neg2sub  8347  divmuleqap  8805  divneg2ap  8824  qapne  9775  seqvalcd  10623  binom2  10813  bcpasc  10928  crim  11239  remullem  11252  max0addsup  11600  summodclem2a  11762  isum1p  11873  geo2sum  11895  cvgratz  11913  efi4p  12098  tanaddap  12120  addcos  12127  cos2tsin  12132  demoivreALT  12155  omeo  12279  sqgcd  12420  eulerthlemth  12624  pythagtriplem16  12672  fldivp1  12741  pockthlem  12749  4sqlem10  12780  gsumval2  13299  grpinvid2  13455  imasgrp2  13516  mulgaddcomlem  13551  mulgmodid  13567  ablsubsub  13724  ablsubsub4  13725  gsumfzsnfd  13751  opprunitd  13942  lmodfopne  14158  mpl0fi  14534  mplnegfi  14537  txrest  14818  limccnpcntop  15217  dvrecap  15255  dvply1  15307  cosq34lt1  15392  wilthlem1  15522  mersenne  15539  lgseisenlem1  15617  lgsquadlem1  15624  lgsquadlem2  15625  lgsquadlem3  15626  lgsquad2lem1  15628  2lgslem1  15638