Theorem 3eqtr2d 2232

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  fmptapd  5750  rdgisucinc  6440  ctm  7170  mulidnq  7451  ltrnqg  7482  recexprlem1ssl  7695  recexprlem1ssu  7696  ltmprr  7704  mulcmpblnrlemg  7802  caucvgsrlemoffcau  7860  negsub  8269  neg2sub  8281  divmuleqap  8738  divneg2ap  8757  qapne  9707  seqvalcd  10535  binom2  10725  bcpasc  10840  crim  11005  remullem  11018  max0addsup  11366  summodclem2a  11527  isum1p  11638  geo2sum  11660  cvgratz  11678  efi4p  11863  tanaddap  11885  addcos  11892  cos2tsin  11897  demoivreALT  11920  omeo  12042  sqgcd  12169  eulerthlemth  12373  pythagtriplem16  12420  fldivp1  12489  pockthlem  12497  4sqlem10  12528  gsumval2  12983  grpinvid2  13128  imasgrp2  13183  mulgaddcomlem  13218  mulgmodid  13234  ablsubsub  13391  ablsubsub4  13392  gsumfzsnfd  13418  opprunitd  13609  lmodfopne  13825  txrest  14455  limccnpcntop  14854  dvrecap  14892  dvply1  14943  cosq34lt1  15026  wilthlem1  15153  lgseisenlem1  15227  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  2lgslem1  15248