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  6661  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  10054  seqvalcd  10918  binom2  11108  bcpasc  11225  hashf1lem2  11307  cats2catd  11562  crim  11644  remullem  11657  max0addsup  12007  summodclem2a  12172  isum1p  12283  geo2sum  12305  cvgratz  12323  efi4p  12508  tanaddap  12530  addcos  12537  cos2tsin  12542  demoivreALT  12565  omeo  12689  sqgcd  12830  eulerthlemth  13038  pythagtriplem16  13086  fldivp1  13155  pockthlem  13163  4sqlem10  13194  ballotfilemscr  13319  ballotfilemfrci  13328  ballotfilemfrceq  13329  gzsumval2  13772  grpinvid2  13916  imasgrp2  13971  mulgaddcomlem  14006  mulgmodid  14022  cntzsgrpcl  14166  cntzsubm  14169  ablsubsub  14211  ablsubsub4  14212  gzsumsnfd  14236  gsum2dfi  14272  opprunitd  14525  lmodfopne  14771  psrass1fi  15210  mpl0fi  15235  mplnegfi  15238  txrest  15519  limccnpcntop  15918  dvrecap  15956  dvply1  16008  cosq34lt1  16095  log2tlbndlog2  16237  birthdaylem2  16243  wilthlem1  16249  mersenne  16314  lgseisenlem1  16411  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem1  16422  2lgslem1  16432  qdiff  17322