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  5900  rdgisucinc  6649  ctm  7442  mulidnq  7749  ltrnqg  7780  recexprlem1ssl  7993  recexprlem1ssu  7994  ltmprr  8002  mulcmpblnrlemg  8100  caucvgsrlemoffcau  8158  negsub  8567  neg2sub  8579  divmuleqap  9040  divneg2ap  9059  qapne  10021  seqvalcd  10879  binom2  11069  bcpasc  11185  hashf1lem2  11267  cats2catd  11522  crim  11604  remullem  11617  max0addsup  11966  summodclem2a  12129  isum1p  12240  geo2sum  12262  cvgratz  12280  efi4p  12465  tanaddap  12487  addcos  12494  cos2tsin  12499  demoivreALT  12522  omeo  12646  sqgcd  12787  eulerthlemth  12991  pythagtriplem16  13039  fldivp1  13108  pockthlem  13116  4sqlem10  13147  ballotfilemscr  13243  ballotfilemfrci  13252  ballotfilemfrceq  13253  gzsumval2  13694  grpinvid2  13838  imasgrp2  13893  mulgaddcomlem  13928  mulgmodid  13944  ablsubsub  14102  ablsubsub4  14103  gzsumsnfd  14127  opprunitd  14393  lmodfopne  14638  mpl0fi  15019  mplnegfi  15022  txrest  15303  limccnpcntop  15702  dvrecap  15740  dvply1  15792  cosq34lt1  15877  wilthlem1  16011  mersenne  16028  lgseisenlem1  16106  lgsquadlem1  16113  lgsquadlem2  16114  lgsquadlem3  16115  lgsquad2lem1  16117  2lgslem1  16127  qdiff  17006