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  5749  rdgisucinc  6438  ctm  7168  mulidnq  7449  ltrnqg  7480  recexprlem1ssl  7693  recexprlem1ssu  7694  ltmprr  7702  mulcmpblnrlemg  7800  caucvgsrlemoffcau  7858  negsub  8267  neg2sub  8279  divmuleqap  8736  divneg2ap  8755  qapne  9704  seqvalcd  10532  binom2  10722  bcpasc  10837  crim  11002  remullem  11015  max0addsup  11363  summodclem2a  11524  isum1p  11635  geo2sum  11657  cvgratz  11675  efi4p  11860  tanaddap  11882  addcos  11889  cos2tsin  11894  demoivreALT  11917  omeo  12039  sqgcd  12166  eulerthlemth  12370  pythagtriplem16  12417  fldivp1  12486  pockthlem  12494  4sqlem10  12525  gsumval2  12980  grpinvid2  13125  imasgrp2  13180  mulgaddcomlem  13215  mulgmodid  13231  ablsubsub  13388  ablsubsub4  13389  gsumfzsnfd  13415  opprunitd  13606  lmodfopne  13822  txrest  14444  limccnpcntop  14829  dvrecap  14862  cosq34lt1  14985  wilthlem1  15112  lgseisenlem1  15186  lgsquadlem1  15191