Theorem 3eqtr2d 2277

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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  fmptapd  5897  rdgisucinc  6646  ctm  7439  mulidnq  7746  ltrnqg  7777  recexprlem1ssl  7990  recexprlem1ssu  7991  ltmprr  7999  mulcmpblnrlemg  8097  caucvgsrlemoffcau  8155  negsub  8564  neg2sub  8576  divmuleqap  9037  divneg2ap  9056  qapne  10018  seqvalcd  10876  binom2  11066  bcpasc  11182  hashf1lem2  11264  cats2catd  11519  crim  11601  remullem  11614  max0addsup  11963  summodclem2a  12126  isum1p  12237  geo2sum  12259  cvgratz  12277  efi4p  12462  tanaddap  12484  addcos  12491  cos2tsin  12496  demoivreALT  12519  omeo  12643  sqgcd  12784  eulerthlemth  12988  pythagtriplem16  13036  fldivp1  13105  pockthlem  13113  4sqlem10  13144  ballotfilemscr  13240  ballotfilemfrci  13249  ballotfilemfrceq  13250  gzsumval2  13691  grpinvid2  13835  imasgrp2  13890  mulgaddcomlem  13925  mulgmodid  13941  ablsubsub  14099  ablsubsub4  14100  gzsumsnfd  14124  opprunitd  14390  lmodfopne  14635  mpl0fi  15016  mplnegfi  15019  txrest  15300  limccnpcntop  15699  dvrecap  15737  dvply1  15789  cosq34lt1  15874  wilthlem1  16008  mersenne  16025  lgseisenlem1  16103  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  2lgslem1  16124  qdiff  17003