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  5906  rdgisucinc  6656  ctm  7450  mulidnq  7757  ltrnqg  7788  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  mulcmpblnrlemg  8108  caucvgsrlemoffcau  8166  negsub  8576  neg2sub  8588  divmuleqap  9050  divneg2ap  9069  qapne  10049  seqvalcd  10913  binom2  11103  bcpasc  11220  hashf1lem2  11302  cats2catd  11557  crim  11639  remullem  11652  max0addsup  12002  summodclem2a  12167  isum1p  12278  geo2sum  12300  cvgratz  12318  efi4p  12503  tanaddap  12525  addcos  12532  cos2tsin  12537  demoivreALT  12560  omeo  12684  sqgcd  12825  eulerthlemth  13033  pythagtriplem16  13081  fldivp1  13150  pockthlem  13158  4sqlem10  13189  ballotfilemscr  13314  ballotfilemfrci  13323  ballotfilemfrceq  13324  gzsumval2  13767  grpinvid2  13911  imasgrp2  13966  mulgaddcomlem  14001  mulgmodid  14017  cntzsgrpcl  14161  cntzsubm  14164  ablsubsub  14206  ablsubsub4  14207  gzsumsnfd  14231  opprunitd  14501  lmodfopne  14747  mpl0fi  15184  mplnegfi  15187  txrest  15468  limccnpcntop  15867  dvrecap  15905  dvply1  15957  cosq34lt1  16043  log2tlbndlog2  16181  birthdaylem2  16187  wilthlem1  16193  mersenne  16258  lgseisenlem1  16355  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem1  16366  2lgslem1  16376  qdiff  17265