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 ⊢ (𝜑 → 𝐴 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fmptapd  5909  rdgisucinc  6660  ctm  7455  mulidnq  7762  ltrnqg  7793  recexprlem1ssl  8006  recexprlem1ssu  8007  ltmprr  8015  mulcmpblnrlemg  8113  caucvgsrlemoffcau  8171  negsub  8581  neg2sub  8593  divmuleqap  9055  divneg2ap  9074  qapne  10055  seqvalcd  10919  binom2  11109  bcpasc  11226  hashf1lem2  11308  cats2catd  11563  crim  11645  remullem  11658  max0addsup  12008  summodclem2a  12173  isum1p  12284  geo2sum  12306  cvgratz  12324  efi4p  12509  tanaddap  12531  addcos  12538  cos2tsin  12543  demoivreALT  12566  omeo  12690  sqgcd  12831  eulerthlemth  13039  pythagtriplem16  13087  fldivp1  13156  pockthlem  13164  4sqlem10  13195  ballotfilemscr  13320  ballotfilemfrci  13329  ballotfilemfrceq  13330  gzsumval2  13773  grpinvid2  13917  imasgrp2  13972  mulgaddcomlem  14007  mulgmodid  14023  cntzsgrpcl  14167  cntzsubm  14170  ablsubsub  14212  ablsubsub4  14213  gzsumsnfd  14237  gsum2dfi  14273  opprunitd  14526  lmodfopne  14772  psrass1fi  15201  mpl0fi  15218  mplnegfi  15221  txrest  15502  limccnpcntop  15901  dvrecap  15939  dvply1  15991  cosq34lt1  16078  log2tlbndlog2  16220  birthdaylem2  16226  wilthlem1  16232  mersenne  16297  lgseisenlem1  16394  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem1  16405  2lgslem1  16415  qdiff  17305