Theorem 3eqtr2d 2777

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  fmptapd  7117  negsub  11429  neg2sub  11441  divmuleq  11846  divneg2  11865  discr  14163  bcpasc  14244  hashgval2  14301  hashf1lem2  14379  relexpaddnn  14974  crim  15038  remullem  15051  isum1p  15764  geo2sum  15796  fallfacfwd  15959  fsumkthpow  15979  bpoly3  15981  bpoly4  15982  efi4p  16062  sinhval  16079  addcos  16099  cos2tsin  16104  demoivreALT  16126  rpnnen2lem11  16149  omeo  16293  pwp1fsum  16318  sadaddlem  16393  bitsres  16400  smumullem  16419  sqgcd  16489  expgcd  16490  eulerthlem2  16709  vfermltlALT  16730  pockthlem  16833  4sqlem10  16875  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  fuccocl  17891  resssetc  18016  resscatc  18033  uncfcurf  18162  yonedalem3b  18202  prdspjmhm  18754  grpinvid2  18922  imasgrp2  18985  mulgaddcomlem  19027  mulgmodid  19043  lagsubg2  19123  cntzsgrpcl  19263  cntzsubm  19267  sylow3lem2  19557  efgredleme  19672  ablsubsub  19746  ablsubsub4  19747  odadd2  19778  gex2abl  19780  pgpfac1lem3a  20007  pwspjmhmmgpd  20263  rngcid  20568  ringcid  20597  abvneg  20759  lmodfopne  20851  lsppr  21045  rngqiprngfulem4  21269  gzrngunit  21388  frlmsubgval  21720  frlmgsum  21727  psrass1  21919  resspsradd  21930  resspsrvsca  21932  mplcoe5  21995  mplmon2mul  22024  evlslem2  22034  evlsvarsrng  22062  coe1tm  22215  ply1scl1OLD  22236  ply1fermltlchr  22256  evls1varsrng  22284  mamuass  22346  mavmulass  22493  mulmarep1gsum2  22518  mdetuni0  22565  maducoeval2  22584  madulid  22589  mat2pmatmul  22675  decpmatmulsumfsupp  22717  pmatcollpwlem  22724  pm2mpmhmlem1  22762  cmpfi  23352  cnconn  23366  txrest  23575  utopsnneiplem  24191  blcvx  24742  tcphcphlem2  25192  cphipval2  25197  cphipval  25199  rrx0  25353  minveclem2  25382  pjthlem1  25393  uniioovol  25536  uniioombllem2  25540  itg1addlem4  25656  mbfi1fseqlem5  25676  itg2mulc  25704  itg2monolem1  25707  itgaddlem1  25780  itgmulc2lem2  25790  dvrec  25915  lhop2  25976  ftc1lem5  26003  deg1submon1p  26114  plypf1  26173  coefv0  26209  coemulhi  26215  coemulc  26216  dgreq0  26227  dvply1  26247  vieta1  26276  aareccl  26290  aaliou3lem8  26309  dvtaylp  26334  mtest  26369  sineq0  26489  efif1olem2  26508  efif1olem4  26510  tanarg  26584  logtayl2  26627  nnlogbexp  26747  isosctrlem2  26785  chordthmlem2  26799  chordthmlem4  26801  heron  26804  dcubic1lem  26809  dcubic1  26811  mcubic  26813  dquart  26819  quart1lem  26821  quart1  26822  efiasin  26854  asinsin  26858  atancj  26876  efiatan  26878  atanlogaddlem  26879  cosatan  26887  atantan  26889  atans2  26897  log2cnv  26910  log2tlbnd  26911  birthdaylem2  26918  cxplim  26938  lgamgulmlem2  26996  wilthlem1  27034  basellem3  27049  musum  27157  musumsum  27158  muinv  27159  pclogsum  27182  mersenne  27194  dchrabs  27227  dchrinv  27228  lgseisenlem1  27342  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2lem1  27351  2lgslem1  27361  2sqmod  27403  chebbnd1lem3  27438  chpchtlim  27446  rplogsumlem2  27452  dchrisumlem2  27457  dchrmusum2  27461  mulog2sumlem1  27501  mulog2sumlem3  27503  vmalogdivsum2  27505  selberg4lem1  27527  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntibndlem2  27558  pntlemr  27569  pntlemf  27572  pntlemo  27574  addsdilem4  28150  mulsunif2lem  28165  halfcut  28454  bdayfinbndlem1  28463  ragcom  28770  colperpexlem1  28802  lmiisolem  28868  hypcgrlem2  28872  trgcopyeulem  28877  brbtwn2  28978  colinearalglem1  28979  colinearalglem2  28980  axcontlem2  29038  axcontlem8  29044  numedglnl  29217  clwlkclwwlklem2a  30073  numclwlk1lem1  30444  numclwlk1lem2  30445  numclwwlk2  30456  grpoinvid2  30604  ablodivdiv4  30629  smcnlem  30772  ipidsq  30785  ipasslem2  30907  minvecolem2  30950  hv2times  31136  pjhthlem1  31466  pjds3i  31788  ho2times  31894  opsqrlem6  32220  pjclem4  32274  pj3si  32282  csmdsymi  32409  ofoprabco  32742  fcnvgreu  32751  quad3d  32829  nn0diffz0  32874  swrdrndisj  33039  trsp2cyc  33205  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2  33215  conjga  33252  elrgspnlem1  33324  rlocmulval  33351  imaslmod  33434  1arithufdlem3  33627  deg1prod  33664  r1padd1  33689  mplvrpmrhm  33712  frlmdim  33768  rrxdim  33771  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  extdg1id  33823  ccfldextdgrr  33829  fldextrspunlem1  33832  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrrecl  33926  constrresqrtcl  33934  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  qqhcn  34148  esumpr2  34224  esumpfinval  34232  esumpfinvalf  34233  carsggect  34475  oddpwdcv  34512  eulerpartlemgs2  34537  fibp1  34558  orvcelval  34626  ballotlemscr  34676  ballotlemfrci  34685  signsplypnf  34707  reprpmtf1o  34783  breprexplemc  34789  breprexp  34790  circlemeth  34797  lpadright  34841  revwlk  35319  subfacp1lem5  35378  cvmliftlem10  35488  circum  35868  faclimlem3  35939  fwddifnp1  36359  bj-bary1lem  37515  tan2h  37813  poimirlem3  37824  poimirlem13  37834  poimirlem14  37835  itgaddnclem1  37879  itgmulc2nclem2  37888  areacirclem1  37909  areacirclem4  37912  istotbnd3  37972  iscringd  38199  3atlem1  39743  pmod2iN  40109  polval2N  40166  lhple  40302  cdleme2  40488  cdleme35d  40712  cdleme42h  40742  cdlemeg46ngfr  40778  cdlemkid1  41182  lcfl7lem  41759  mapdpglem22  41953  mapdh6dN  41999  hdmap1l6d  42073  hdmapinvlem3  42180  lcmineqlem3  42285  nnadddir  42525  readvrec2  42616  readdsub  42639  sn-negex12  42672  zmulcomlem  42722  selvvvval  42828  evlselv  42830  evlsmhpvvval  42838  prjspeclsp  42855  prjspner1  42869  3cubeslem3r  42929  diophin  43014  irrapxlem2  43065  pellexlem6  43076  pell1234qrmulcl  43097  rmxyval  43157  rmxyneg  43162  rmxyadd  43163  jm2.24  43205  jm2.25  43241  limexissupab  43525  omabs2  43574  tfsconcatrev  43590  naddwordnexlem4  43643  snhesn  44027  scottrankd  44489  radcnvrat  44555  binomcxplemnotnn0  44597  sub2times  45521  mul13d  45528  fperiodmullem  45551  fperiodmul  45552  isumneg  45848  climneg  45856  itgsinexp  46199  stoweidlem13  46257  stoweidlem42  46286  wallispilem4  46312  wallispilem5  46313  wallispi2lem1  46315  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem7  46324  stirlinglem10  46327  dirkertrigeqlem3  46344  fourierdlem30  46381  fourierdlem32  46383  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem83  46433  sqwvfoura  46472  sqwvfourb  46473  etransclem2  46480  etransclem46  46524  sharhght  47109  imasetpreimafvbijlemfv  47648  fmtnorec3  47794  quad1  47866  requad1  47868  ushggricedg  48173  lmodvsmdi  48625  dmatALTbas  48647  ldepsprlem  48718  itcovalt2lem2lem2  48920  ackval3  48929  1subrec1sub  48951  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  itsclc0xyqsolr  49015  swapfid  49524  sinhpcosh  49985