Theorem 3eqtr2d 2235

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fmptapd  5756  rdgisucinc  6452  ctm  7184  mulidnq  7475  ltrnqg  7506  recexprlem1ssl  7719  recexprlem1ssu  7720  ltmprr  7728  mulcmpblnrlemg  7826  caucvgsrlemoffcau  7884  negsub  8293  neg2sub  8305  divmuleqap  8763  divneg2ap  8782  qapne  9732  seqvalcd  10572  binom2  10762  bcpasc  10877  crim  11042  remullem  11055  max0addsup  11403  summodclem2a  11565  isum1p  11676  geo2sum  11698  cvgratz  11716  efi4p  11901  tanaddap  11923  addcos  11930  cos2tsin  11935  demoivreALT  11958  omeo  12082  sqgcd  12223  eulerthlemth  12427  pythagtriplem16  12475  fldivp1  12544  pockthlem  12552  4sqlem10  12583  gsumval2  13101  grpinvid2  13257  imasgrp2  13318  mulgaddcomlem  13353  mulgmodid  13369  ablsubsub  13526  ablsubsub4  13527  gsumfzsnfd  13553  opprunitd  13744  lmodfopne  13960  mpl0fi  14336  mplnegfi  14339  txrest  14620  limccnpcntop  15019  dvrecap  15057  dvply1  15109  cosq34lt1  15194  wilthlem1  15324  mersenne  15341  lgseisenlem1  15419  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem1  15430  2lgslem1  15440