Theorem 3eqtr2d 2821

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

Syntax hints:   → wi 4   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2772

This theorem is referenced by:  fmptapd  6756  negsub  10735  neg2sub  10747  divmuleq  11146  divneg2  11165  discr  13416  bcpasc  13496  hashgval2  13552  hashf1lem2  13627  relexpaddnn  14271  crim  14335  remullem  14348  isum1p  15056  geo2sum  15089  fallfacfwd  15250  fsumkthpow  15270  bpoly3  15272  bpoly4  15273  efi4p  15350  sinhval  15367  addcos  15387  cos2tsin  15392  demoivreALT  15414  rpnnen2lem11  15437  omeo  15575  pwp1fsum  15602  sadaddlem  15675  bitsres  15682  smumullem  15701  sqgcd  15765  eulerthlem2  15975  vfermltlALT  15995  pockthlem  16097  4sqlem10  16139  vdwlem2  16174  vdwlem6  16178  vdwlem8  16180  fuccocl  17092  resssetc  17210  resscatc  17223  uncfcurf  17347  yonedalem3b  17387  prdspjmhm  17835  grpinvid2  17942  imasgrp2  18001  mulgaddcomlem  18034  mulgmodid  18050  lagsubg2  18124  cntzsubm  18237  sylow3lem2  18514  efgredleme  18628  ablsubsub  18696  ablsubsub4  18697  odadd2  18725  gex2abl  18727  pgpfac1lem3a  18948  abvneg  19327  lmodfopne  19394  lsppr  19587  psrass1  19899  resspsradd  19910  resspsrvsca  19912  mplcoe5  19962  mplmon2mul  19994  evlslem2  20005  evlsvarsrng  20021  coe1tm  20144  ply1scl1  20163  evls1varsrng  20205  gzrngunit  20313  frlmsubgval  20611  frlmgsum  20618  mamuass  20715  mavmulass  20862  mulmarep1gsum2  20887  mdetuni0  20934  maducoeval2  20953  madulid  20958  mat2pmatmul  21043  decpmatmulsumfsupp  21085  pmatcollpwlem  21092  pm2mpmhmlem1  21130  cmpfi  21720  cnconn  21734  txrest  21943  utopsnneiplem  22559  blcvx  23109  tcphcphlem2  23542  cphipval2  23547  cphipval  23549  rrx0  23703  minveclem2  23732  pjthlem1  23743  uniioovol  23883  uniioombllem2  23887  itg1addlem4  24003  mbfi1fseqlem5  24023  itg2mulc  24051  itg2monolem1  24054  itgaddlem1  24126  itgmulc2lem2  24136  dvrec  24255  lhop2  24315  ftc1lem5  24340  deg1submon1p  24449  plypf1  24505  coefv0  24541  coemulhi  24547  coemulc  24548  dgreq0  24558  dvply1  24576  vieta1  24604  aareccl  24618  aaliou3lem8  24637  dvtaylp  24661  mtest  24695  sineq0  24812  efif1olem2  24828  efif1olem4  24830  tanarg  24903  logtayl2  24946  nnlogbexp  25060  isosctrlem2  25098  chordthmlem2  25112  chordthmlem4  25114  heron  25117  dcubic1lem  25122  dcubic1  25124  mcubic  25126  dquart  25132  quart1lem  25134  quart1  25135  efiasin  25167  asinsin  25171  atancj  25189  efiatan  25191  atanlogaddlem  25192  cosatan  25200  atantan  25202  atans2  25210  log2cnv  25224  log2tlbnd  25225  birthdaylem2  25232  cxplim  25251  lgamgulmlem2  25309  wilthlem1  25347  basellem3  25362  musum  25470  musumsum  25471  muinv  25472  pclogsum  25493  mersenne  25505  dchrabs  25538  dchrinv  25539  lgseisenlem1  25653  lgsquadlem1  25658  lgsquadlem2  25659  lgsquadlem3  25660  lgsquad2lem1  25662  2lgslem1  25672  2sqmod  25714  chebbnd1lem3  25749  chpchtlim  25757  rplogsumlem2  25763  dchrisumlem2  25768  dchrmusum2  25772  mulog2sumlem1  25812  mulog2sumlem3  25814  vmalogdivsum2  25816  selberg4lem1  25838  pntrlog2bndlem2  25856  pntrlog2bndlem4  25858  pntibndlem2  25869  pntlemr  25880  pntlemf  25883  pntlemo  25885  ragcom  26186  colperpexlem1  26218  lmiisolem  26284  hypcgrlem2  26288  trgcopyeulem  26293  brbtwn2  26394  colinearalglem1  26395  colinearalglem2  26396  axcontlem2  26454  axcontlem8  26460  numedglnl  26632  clwlkclwwlklem2a  27504  numclwlk1lem1  27922  numclwlk1lem2  27923  numclwwlk2  27938  grpoinvid2  28083  ablodivdiv4  28108  smcnlem  28251  ipidsq  28264  ipasslem2  28386  minvecolem2  28430  hv2times  28617  pjhthlem1  28949  pjds3i  29271  ho2times  29377  opsqrlem6  29703  pjclem4  29757  pj3si  29765  csmdsymi  29892  ofoprabco  30171  fcnvgreu  30180  imaslmod  30598  frlmdim  30635  rrxdim  30638  lbsdiflsp0  30648  fedgmullem1  30651  fedgmullem2  30652  extdg1id  30679  ccfldextdgrr  30683  qqhcn  30873  esumpr2  30967  esumpfinval  30975  esumpfinvalf  30976  carsggect  31218  oddpwdcv  31255  eulerpartlemgs2  31280  fibp1  31302  orvcelval  31369  ballotlemscr  31419  ballotlemfrci  31428  signsplypnf  31463  reprpmtf1o  31542  breprexplemc  31548  breprexp  31549  circlemeth  31556  lpadright  31600  subfacp1lem5  32013  cvmliftlem10  32123  circum  32434  faclimlem3  32494  fwddifnp1  33144  bj-bary1lem  34036  tan2h  34322  poimirlem3  34333  poimirlem13  34343  poimirlem14  34344  itgaddnclem1  34388  itgmulc2nclem2  34397  areacirclem1  34420  areacirclem4  34423  istotbnd3  34488  iscringd  34715  3atlem1  36061  pmod2iN  36427  polval2N  36484  lhple  36620  cdleme2  36806  cdleme35d  37030  cdleme42h  37060  cdlemeg46ngfr  37096  cdlemkid1  37500  lcfl7lem  38077  mapdpglem22  38271  mapdh6dN  38317  hdmap1l6d  38391  hdmapinvlem3  38498  expgcd  38612  readdsub  38644  prjspeclsp  38666  diophin  38762  irrapxlem2  38813  pellexlem6  38824  pell1234qrmulcl  38845  rmxyval  38905  rmxyneg  38910  rmxyadd  38911  jm2.24  38953  jm2.25  38989  snhesn  39492  scottrankd  39956  radcnvrat  40059  binomcxplemnotnn0  40101  sub2times  40967  mul13d  40972  fperiodmullem  40997  fperiodmul  40998  isumneg  41312  climneg  41320  itgsinexp  41668  stoweidlem13  41727  stoweidlem42  41756  wallispilem4  41782  wallispilem5  41783  wallispi2lem1  41785  stirlinglem1  41788  stirlinglem3  41790  stirlinglem4  41791  stirlinglem5  41792  stirlinglem7  41794  stirlinglem10  41797  dirkertrigeqlem3  41814  fourierdlem30  41851  fourierdlem32  41853  fourierdlem42  41863  fourierdlem48  41868  fourierdlem49  41869  fourierdlem83  41903  sqwvfoura  41942  sqwvfourb  41943  etransclem2  41950  etransclem46  41994  sharhght  42551  fmtnorec3  43076  quad1  43151  requad1  43153  isomgreqve  43356  ushrisomgr  43372  rngcid  43612  ringcid  43658  lmodvsmdi  43794  dmatALTbas  43821  ldepsprlem  43892  1subrec1sub  44058  eenglngeehlnmlem1  44090  eenglngeehlnmlem2  44091  itsclc0xyqsolr  44122  sinhpcosh  44204