Theorem 3eqtr2d 2802

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  fmptapd  7150  negsub  11473  neg2sub  11485  divmuleq  11890  divneg2  11909  nnadddir  12263  discr  14247  bcpasc  14328  hashgval2  14385  hashf1lem2  14463  relexpaddnn  15058  crim  15133  remullem  15146  isum1p  15862  geo2sum  15894  fallfacfwd  16057  fsumkthpow  16077  bpoly3  16079  bpoly4  16080  efi4p  16160  sinhval  16177  addcos  16197  cos2tsin  16202  demoivreALT  16224  rpnnen2lem11  16247  omeo  16391  pwp1fsum  16416  sadaddlem  16491  bitsres  16498  smumullem  16517  sqgcd  16587  expgcd  16588  eulerthlem2  16808  vfermltlALT  16829  pockthlem  16932  4sqlem10  16974  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  fuccocl  17991  resssetc  18116  resscatc  18133  uncfcurf  18262  yonedalem3b  18302  prdspjmhm  18854  grpinvid2  19025  imasgrp2  19088  mulgaddcomlem  19130  mulgmodid  19146  lagsubg2  19226  cntzsgrpcl  19365  cntzsubm  19369  sylow3lem2  19659  efgredleme  19774  ablsubsub  19848  ablsubsub4  19849  odadd2  19880  gex2abl  19882  pgpfac1lem3a  20109  pwspjmhmmgpd  20363  rngcid  20672  ringcid  20701  abvneg  20863  lmodfopne  20955  lsppr  21148  rngqiprngfulem4  21372  gzrngunit  21473  frlmsubgval  21805  frlmgsum  21812  psrass1  22003  resspsradd  22014  resspsrvsca  22016  mplcoe5  22081  mplmon2mul  22110  evlslem2  22120  evlsvarsrng  22148  selvvvval  22183  coe1tm  22324  ply1fermltlchr  22363  evls1varsrng  22391  mamuass  22450  mavmulass  22597  mulmarep1gsum2  22622  mdetuni0  22669  maducoeval2  22688  madulid  22693  mat2pmatmul  22779  decpmatmulsumfsupp  22821  pmatcollpwlem  22828  pm2mpmhmlem1  22866  cmpfi  23456  cnconn  23470  txrest  23679  utopsnneiplem  24295  blcvx  24846  tcphcphlem2  25286  cphipval2  25291  cphipval  25293  rrx0  25447  minveclem2  25476  pjthlem1  25487  uniioovol  25629  uniioombllem2  25633  itg1addlem4  25749  mbfi1fseqlem5  25769  itg2mulc  25797  itg2monolem1  25800  itgaddlem1  25873  itgmulc2lem2  25883  dvrec  26005  lhop2  26065  ftc1lem5  26090  deg1submon1p  26201  plypf1  26260  coefv0  26296  coemulhi  26302  coemulc  26303  dgreq0  26313  dvply1  26336  vieta1  26364  aareccl  26378  aaliou3lem8  26397  dvtaylp  26421  mtest  26455  sineq0  26577  efif1olem2  26596  efif1olem4  26598  tanarg  26672  logtayl2  26715  nnlogbexp  26834  isosctrlem2  26872  chordthmlem2  26886  chordthmlem4  26888  heron  26891  dcubic1lem  26896  dcubic1  26898  mcubic  26900  dquart  26906  quart1lem  26908  quart1  26909  efiasin  26941  asinsin  26945  atancj  26963  efiatan  26965  atanlogaddlem  26966  cosatan  26974  atantan  26976  atans2  26984  log2cnv  26997  log2tlbnd  26998  birthdaylem2  27005  cxplim  27024  lgamgulmlem2  27082  wilthlem1  27120  basellem3  27135  musum  27243  musumsum  27244  muinv  27245  pclogsum  27267  mersenne  27279  dchrabs  27312  dchrinv  27313  lgseisenlem1  27427  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  lgsquad2lem1  27436  2lgslem1  27446  2sqmod  27488  chebbnd1lem3  27523  chpchtlim  27531  rplogsumlem2  27537  dchrisumlem2  27542  dchrmusum2  27546  mulog2sumlem1  27586  mulog2sumlem3  27588  vmalogdivsum2  27590  selberg4lem1  27612  pntrlog2bndlem2  27630  pntrlog2bndlem4  27632  pntibndlem2  27643  pntlemr  27654  pntlemf  27657  pntlemo  27659  addsdilem4  28235  mulsunif2lem  28250  halfcut  28539  bdayfinbndlem1  28548  ragcom  28855  colperpexlem1  28887  lmiisolem  28953  hypcgrlem2  28957  trgcopyeulem  28962  brbtwn2  29063  colinearalglem1  29064  colinearalglem2  29065  axcontlem2  29123  axcontlem8  29129  numedglnl  29302  clwlkclwwlklem2a  30157  numclwlk1lem1  30528  numclwlk1lem2  30529  numclwwlk2  30540  grpoinvid2  30689  ablodivdiv4  30714  smcnlem  30857  ipidsq  30870  ipasslem2  30992  minvecolem2  31035  hv2times  31221  pjhthlem1  31551  pjds3i  31873  ho2times  31979  opsqrlem6  32305  pjclem4  32359  pj3si  32367  csmdsymi  32494  ofoprabco  32827  fcnvgreu  32835  quad3d  32912  nn0diffz0  32957  swrdrndisj  33096  trsp2cyc  33264  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2  33274  conjga  33311  elrgspnlem1  33384  rlocmulval  33412  rlocinvunit  33417  rlocisunit  33418  imaslmod  33500  1arithufdlem3  33703  deg1prod  33740  r1padd1  33765  selvply1rhmlem2  33779  mplvrpmrhm  33805  esplyfvaln  33832  frlmdim  33869  rrxdim  33872  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  extdg1id  33924  ccfldextdgrr  33930  fldextrspunlem1  33933  constrrtlc1  33990  constrrtcclem  33992  constrrtcc  33993  constrrecl  34027  constrresqrtcl  34035  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminplylem3  34042  cos9thpiminply  34046  qqhcn  34249  esumpr2  34325  esumpfinval  34333  esumpfinvalf  34334  carsggect  34576  oddpwdcv  34613  eulerpartlemgs2  34638  fibp1  34659  orvcelval  34727  ballotlemscr  34777  ballotlemfrci  34786  signsplypnf  34805  reprpmtf1o  34881  breprexplemc  34887  breprexp  34888  circlemeth  34895  lpadright  34942  revwlk  35436  subfacp1lem5  35495  cvmliftlem10  35605  circum  35985  faclimlem3  36056  fwddifnp1  36476  bj-bary1lem  37763  qdiff  37780  tan2h  38072  poimirlem3  38083  poimirlem13  38093  poimirlem14  38094  itgaddnclem1  38138  itgmulc2nclem2  38147  areacirclem1  38168  areacirclem4  38171  istotbnd3  38231  iscringd  38458  3atlem1  40068  pmod2iN  40434  polval2N  40491  lhple  40627  cdleme2  40813  cdleme35d  41037  cdleme42h  41067  cdlemeg46ngfr  41103  cdlemkid1  41507  lcfl7lem  42084  mapdpglem22  42278  mapdh6dN  42324  hdmap1l6d  42398  hdmapinvlem3  42505  lcmineqlem3  42609  readvrec2  42931  readdsub  42954  sn-negex12  42987  zmulcomlem  43050  evlselv  43132  evlsmhpvvval  43138  prjspeclsp  43155  prjspner1  43169  3cubeslem3r  43229  diophin  43314  irrapxlem2  43361  pellexlem6  43372  pell1234qrmulcl  43393  rmxyval  43453  rmxyneg  43458  rmxyadd  43459  jm2.24  43501  jm2.25  43537  limexissupab  43821  omabs2  43870  tfsconcatrev  43886  naddwordnexlem4  43939  snhesn  44323  scottrankd  44785  radcnvrat  44851  binomcxplemnotnn0  44893  sub2times  45813  mul13d  45820  fperiodmullem  45843  fperiodmul  45844  isumneg  46139  climneg  46147  itgsinexp  46490  stoweidlem13  46548  stoweidlem42  46577  wallispilem4  46603  wallispilem5  46604  wallispi2lem1  46606  stirlinglem1  46609  stirlinglem3  46611  stirlinglem4  46612  stirlinglem5  46613  stirlinglem7  46615  stirlinglem10  46618  dirkertrigeqlem3  46635  fourierdlem30  46672  fourierdlem32  46674  fourierdlem42  46684  fourierdlem48  46689  fourierdlem49  46690  fourierdlem83  46724  sqwvfoura  46763  sqwvfourb  46764  etransclem2  46771  etransclem46  46815  sharhght  47400  sin3t  47426  sin5tlem1  47428  sin5tlem3  47430  cos5t  47434  imasetpreimafvbijlemfv  47969  fmtnorec3  48118  quad1  48203  requad1  48205  ushggricedg  48510  lmodvsmdi  48962  dmatALTbas  48984  ldepsprlem  49055  itcovalt2lem2lem2  49257  ackval3  49266  1subrec1sub  49288  eenglngeehlnmlem1  49320  eenglngeehlnmlem2  49321  itsclc0xyqsolr  49352  swapfid  49861  sinhpcosh  50322