Theorem 3eqtr2d 2804

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  fmptapd  7207  scottrankd  9986  negsub  11645  neg2sub  11657  divmuleq  12062  divneg2  12081  nnadddir  12434  addmuldir2d  14396  discr  14425  bcpasc  14506  hashgval2  14563  hashf1lem2  14642  relexpaddnn  15247  crim  15325  remullem  15338  isum1p  16054  geo2sum  16086  fallfacfwd  16246  fsumkthpow  16266  bpoly3  16268  bpoly4  16269  efi4p  16349  sinhval  16366  addcos  16386  cos2tsin  16391  demoivreALT  16413  rpnnen2lem11  16436  omeo  16580  pwp1fsum  16605  sadaddlem  16680  bitsres  16687  smumullem  16706  sqgcd  16780  expgcd  16781  eulerthlem2  17003  vfermltlALT  17024  pockthlem  17127  4sqlem10  17169  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  fuccocl  18192  resssetc  18317  resscatc  18334  uncfcurf  18463  yonedalem3b  18503  prdspjmhm  19075  grpinvid2  19253  imasgrp2  19315  mulgaddcomlem  19357  mulgmodid  19373  lagsubg2  19459  cntzsgrpcl  19599  cntzsubm  19603  sylow3lem2  19893  efgredleme  20008  ablsubsub  20082  ablsubsub4  20083  odadd2  20114  gex2abl  20116  pgpfac1lem3a  20343  pwspjmhmmgpd  20608  rngcid  20938  ringcid  20967  abvneg  21134  lmodfopne  21226  lsppr  21419  rngqiprngfulem4  21661  gzrngunit  21793  frlmsubgval  22126  frlmgsum  22133  psrass1  22326  resspsradd  22337  resspsrvsca  22339  mplcoe5  22404  mplmon2mul  22433  evlslem2  22443  evlsvarsrng  22471  selvvvval  22506  coe1tm  22647  ply1fermltlchr  22685  evls1varsrng  22713  mamuass  22772  mavmulass  22919  mulmarep1gsum2  22944  mdetuni0  22991  maducoeval2  23010  madulid  23015  mat2pmatmul  23104  decpmatmulsumfsupp  23146  pmatcollpwlem  23153  pm2mpmhmlem1  23191  cmpfi  23781  cnconn  23795  txrest  24005  utopsnneiplem  24621  blcvx  25172  tcphcphlem2  25612  cphipval2  25617  cphipval  25619  rrx0  25773  minveclem2  25802  pjthlem1  25813  uniioovol  25955  uniioombllem2  25959  itg1addlem4  26075  mbfi1fseqlem5  26095  itg2mulc  26123  itg2monolem1  26126  itgaddlem1  26198  itgmulc2lem2  26208  dvrec  26330  lhop2  26390  ftc1lem5  26415  deg1submon1p  26526  plypf1  26586  coefv0  26622  coemulhi  26628  coemulc  26629  dgreq0  26639  dvply1  26660  vieta1  26690  aareccl  26710  aaliou3lem8  26729  dvtaylp  26754  mtest  26788  sineq0  26909  efif1olem2  26928  efif1olem4  26930  tanarg  27004  logtayl2  27047  nnlogbexp  27166  isosctrlem2  27204  chordthmlem2  27218  chordthmlem4  27220  heron  27223  dcubic1lem  27228  dcubic1  27230  mcubic  27232  dquart  27238  quart1lem  27240  quart1  27241  efiasin  27273  asinsin  27277  atancj  27295  efiatan  27297  atanlogaddlem  27298  cosatan  27306  atantan  27308  atans2  27316  log2cnv  27329  log2tlbnd  27330  birthdaylem2  27337  cxplim  27356  lgamgulmlem2  27414  wilthlem1  27452  basellem3  27467  musum  27575  musumsum  27576  muinv  27577  pclogsum  27599  mersenne  27611  dchrabs  27644  dchrinv  27645  lgseisenlem1  27759  lgsquadlem1  27764  lgsquadlem2  27765  lgsquadlem3  27766  lgsquad2lem1  27768  2lgslem1  27778  2sqmod  27820  chebbnd1lem3  27855  chpchtlim  27863  rplogsumlem2  27869  dchrisumlem2  27874  dchrmusum2  27878  mulog2sumlem1  27918  mulog2sumlem3  27920  vmalogdivsum2  27922  selberg4lem1  27944  pntrlog2bndlem2  27962  pntrlog2bndlem4  27964  pntibndlem2  27975  pntlemr  27986  pntlemf  27989  pntlemo  27991  addsdilem4  28597  mulsunif2lem  28612  halfcut  28901  bdayfinbndlem1  28910  ragcom  29230  colperpexlem1  29263  plngrotlem2  29323  plng3p  29332  lmiisolem  29358  hypcgrlem2  29363  trgcopyeulem  29369  brbtwn2  29540  colinearalglem1  29541  colinearalglem2  29542  axcontlem2  29600  axcontlem8  29606  numedglnl  29779  revwlk  30324  clwlkclwwlklem2a  30646  numclwlk1lem1  31027  numclwlk1lem2  31028  numclwwlk2  31039  grpoinvid2  31188  ablodivdiv4  31213  smcnlem  31356  ipidsq  31369  ipasslem2  31491  minvecolem2  31534  hv2times  31720  pjhthlem1  32050  pjds3i  32372  ho2times  32478  opsqrlem6  32804  pjclem4  32858  pj3si  32866  csmdsymi  32993  ofoprabco  33356  fcnvgreu  33364  quad3d  33437  nn0diffz0  33482  swrdrndisj  33614  trsp2cyc  33783  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2  33793  conjga  33830  elrgspnlem1  33902  rlocmulval  33930  rlocinvunit  33935  rlocisunit  33936  imaslmod  34018  1arithufdlem3  34182  deg1prod  34218  r1padd1  34245  rngunsnply1chr2lem2  34251  rngunsnply1chr2  34253  selvply1rhmlem2  34264  mplvrpmrhm  34290  esplyfvaln  34317  frlmdim  34354  rrxdim  34357  lbsdiflsp0  34369  fedgmullem1  34372  fedgmullem2  34373  extdg1id  34409  ccfldextdgrr  34415  fldextrspunlem1  34418  constrrtlc1  34475  constrrtcclem  34477  constrrtcc  34478  constrrecl  34512  constrresqrtcl  34520  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  qqhcn  34734  esumpr2  34810  esumpfinval  34818  esumpfinvalf  34819  carsggect  35061  oddpwdcv  35098  eulerpartlemgs2  35123  fibp1  35144  orvcelval  35212  ballotlemscr  35262  ballotlemfrci  35271  signsplypnf  35290  reprpmtf1o  35366  breprexplemc  35372  breprexp  35373  circlemeth  35380  lpadright  35427  subfacp1lem5  36157  cvmliftlem10  36267  circum  36647  faclimlem3  36725  fwddifnp1  37145  bj-bary1lem  38499  qdiff  38516  tan2h  38803  poimirlem3  38809  poimirlem13  38819  poimirlem14  38820  itgaddnclem1  38864  itgmulc2nclem2  38873  areacirclem1  38894  areacirclem4  38897  istotbnd3  38971  iscringd  39198  3atlem1  40806  pmod2iN  41172  polval2N  41229  lhple  41365  cdleme2  41551  cdleme35d  41775  cdleme42h  41805  cdlemeg46ngfr  41841  cdlemkid1  42245  lcfl7lem  42822  mapdpglem22  43016  mapdh6dN  43062  hdmap1l6d  43136  hdmapinvlem3  43243  lcmineqlem3  43347  readvrec2  43678  readdsub  43701  sn-negex12  43734  zmulcomlem  43797  evlselv  43883  evlsmhpvvval  43889  prjspeclsp  43906  3cubeslem3r  43963  diophin  44049  irrapxlem2  44096  pellexlem6  44107  pell1234qrmulcl  44128  rmxyval  44188  rmxyneg  44193  rmxyadd  44194  jm2.24  44236  jm2.25  44272  limexissupab  44546  omabs2  44595  tfsconcatrev  44611  naddwordnexlem4  44664  snhesn  45047  radcnvrat  45559  binomcxplemnotnn0  45601  sub2times  46562  mul13d  46569  fperiodmullem  46592  fperiodmul  46593  isumneg  46887  climneg  46895  itgsinexp  47238  stoweidlem13  47296  stoweidlem42  47325  wallispilem4  47351  wallispilem5  47352  wallispi2lem1  47354  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem5  47361  stirlinglem7  47363  stirlinglem10  47366  dirkertrigeqlem3  47383  fourierdlem30  47420  fourierdlem32  47422  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem83  47472  sqwvfoura  47511  sqwvfourb  47512  etransclem2  47519  etransclem46  47563  sharhght  48148  sin3t  48190  sin5tlem1  48192  sin5tlem3  48194  cos5t  48198  imasetpreimafvbijlemfv  48757  fmtnorec3  48906  quad1  48991  requad1  48993  ushggricedg  49298  lmodvsmdi  49822  dmatALTbas  49844  ldepsprlem  49915  itcovalt2lem2lem2  50117  ackval3  50126  1subrec1sub  50148  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  itsclc0xyqsolr  50212  swapfid  50732  sinhpcosh  51238  sinhneg  51242  coshsinhsq  51260  ontanhsq  51261