Theorem 3eqtr2d 2226

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

Syntax hints:   → wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  fmptapd  5720  rdgisucinc  6399  ctm  7121  mulidnq  7401  ltrnqg  7432  recexprlem1ssl  7645  recexprlem1ssu  7646  ltmprr  7654  mulcmpblnrlemg  7752  caucvgsrlemoffcau  7810  negsub  8218  neg2sub  8230  divmuleqap  8687  divneg2ap  8706  qapne  9652  seqvalcd  10472  binom2  10645  bcpasc  10759  crim  10880  remullem  10893  max0addsup  11241  summodclem2a  11402  isum1p  11513  geo2sum  11535  cvgratz  11553  efi4p  11738  tanaddap  11760  addcos  11767  cos2tsin  11772  demoivreALT  11794  omeo  11916  sqgcd  12043  eulerthlemth  12245  pythagtriplem16  12292  fldivp1  12359  pockthlem  12367  4sqlem10  12398  grpinvid2  12949  imasgrp2  13004  mulgaddcomlem  13037  mulgmodid  13053  ablsubsub  13154  ablsubsub4  13155  opprunitd  13353  lmodfopne  13510  txrest  14047  limccnpcntop  14415  dvrecap  14448  cosq34lt1  14542  lgseisenlem1  14721