Theorem 3eqtr2d 2779

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  fmptapd  7169  negsub  11508  neg2sub  11520  divmuleq  11919  divneg2  11938  discr  14203  bcpasc  14281  hashgval2  14338  hashf1lem2  14417  relexpaddnn  14998  crim  15062  remullem  15075  isum1p  15787  geo2sum  15819  fallfacfwd  15980  fsumkthpow  16000  bpoly3  16002  bpoly4  16003  efi4p  16080  sinhval  16097  addcos  16117  cos2tsin  16122  demoivreALT  16144  rpnnen2lem11  16167  omeo  16309  pwp1fsum  16334  sadaddlem  16407  bitsres  16414  smumullem  16433  sqgcd  16502  eulerthlem2  16715  vfermltlALT  16735  pockthlem  16838  4sqlem10  16880  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  fuccocl  17917  resssetc  18042  resscatc  18059  uncfcurf  18192  yonedalem3b  18232  prdspjmhm  18710  grpinvid2  18877  imasgrp2  18938  mulgaddcomlem  18977  mulgmodid  18993  lagsubg2  19071  cntzsgrpcl  19198  cntzsubm  19202  sylow3lem2  19496  efgredleme  19611  ablsubsub  19685  ablsubsub4  19686  odadd2  19717  gex2abl  19719  pgpfac1lem3a  19946  pwspjmhmmgpd  20141  abvneg  20442  lmodfopne  20510  lsppr  20704  gzrngunit  21011  frlmsubgval  21320  frlmgsum  21327  psrass1  21525  resspsradd  21536  resspsrvsca  21538  mplcoe5  21595  mplmon2mul  21630  evlslem2  21642  evlsvarsrng  21662  coe1tm  21795  ply1scl1OLD  21816  evls1varsrng  21859  mamuass  21902  mavmulass  22051  mulmarep1gsum2  22076  mdetuni0  22123  maducoeval2  22142  madulid  22147  mat2pmatmul  22233  decpmatmulsumfsupp  22275  pmatcollpwlem  22282  pm2mpmhmlem1  22320  cmpfi  22912  cnconn  22926  txrest  23135  utopsnneiplem  23752  blcvx  24314  tcphcphlem2  24753  cphipval2  24758  cphipval  24760  rrx0  24914  minveclem2  24943  pjthlem1  24954  uniioovol  25096  uniioombllem2  25100  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem5  25237  itg2mulc  25265  itg2monolem1  25268  itgaddlem1  25340  itgmulc2lem2  25350  dvrec  25472  lhop2  25532  ftc1lem5  25557  deg1submon1p  25670  plypf1  25726  coefv0  25762  coemulhi  25768  coemulc  25769  dgreq0  25779  dvply1  25797  vieta1  25825  aareccl  25839  aaliou3lem8  25858  dvtaylp  25882  mtest  25916  sineq0  26033  efif1olem2  26052  efif1olem4  26054  tanarg  26127  logtayl2  26170  nnlogbexp  26286  isosctrlem2  26324  chordthmlem2  26338  chordthmlem4  26340  heron  26343  dcubic1lem  26348  dcubic1  26350  mcubic  26352  dquart  26358  quart1lem  26360  quart1  26361  efiasin  26393  asinsin  26397  atancj  26415  efiatan  26417  atanlogaddlem  26418  cosatan  26426  atantan  26428  atans2  26436  log2cnv  26449  log2tlbnd  26450  birthdaylem2  26457  cxplim  26476  lgamgulmlem2  26534  wilthlem1  26572  basellem3  26587  musum  26695  musumsum  26696  muinv  26697  pclogsum  26718  mersenne  26730  dchrabs  26763  dchrinv  26764  lgseisenlem1  26878  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem1  26887  2lgslem1  26897  2sqmod  26939  chebbnd1lem3  26974  chpchtlim  26982  rplogsumlem2  26988  dchrisumlem2  26993  dchrmusum2  26997  mulog2sumlem1  27037  mulog2sumlem3  27039  vmalogdivsum2  27041  selberg4lem1  27063  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  pntibndlem2  27094  pntlemr  27105  pntlemf  27108  pntlemo  27110  addsdilem4  27609  ragcom  27949  colperpexlem1  27981  lmiisolem  28047  hypcgrlem2  28051  trgcopyeulem  28056  brbtwn2  28163  colinearalglem1  28164  colinearalglem2  28165  axcontlem2  28223  axcontlem8  28229  numedglnl  28404  clwlkclwwlklem2a  29251  numclwlk1lem1  29622  numclwlk1lem2  29623  numclwwlk2  29634  grpoinvid2  29782  ablodivdiv4  29807  smcnlem  29950  ipidsq  29963  ipasslem2  30085  minvecolem2  30128  hv2times  30314  pjhthlem1  30644  pjds3i  30966  ho2times  31072  opsqrlem6  31398  pjclem4  31452  pj3si  31460  csmdsymi  31587  ofoprabco  31889  fcnvgreu  31898  swrdrndisj  32121  trsp2cyc  32282  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  imaslmod  32468  ply1fermltlchr  32662  frlmdim  32696  rrxdim  32699  lbsdiflsp0  32711  fedgmullem1  32714  fedgmullem2  32715  extdg1id  32742  ccfldextdgrr  32746  qqhcn  32971  esumpr2  33065  esumpfinval  33073  esumpfinvalf  33074  carsggect  33317  oddpwdcv  33354  eulerpartlemgs2  33379  fibp1  33400  orvcelval  33467  ballotlemscr  33517  ballotlemfrci  33526  signsplypnf  33561  reprpmtf1o  33638  breprexplemc  33644  breprexp  33645  circlemeth  33652  lpadright  33696  revwlk  34115  subfacp1lem5  34175  cvmliftlem10  34285  circum  34659  faclimlem3  34715  fwddifnp1  35137  bj-bary1lem  36191  tan2h  36480  poimirlem3  36491  poimirlem13  36501  poimirlem14  36502  itgaddnclem1  36546  itgmulc2nclem2  36555  areacirclem1  36576  areacirclem4  36579  istotbnd3  36639  iscringd  36866  3atlem1  38354  pmod2iN  38720  polval2N  38777  lhple  38913  cdleme2  39099  cdleme35d  39323  cdleme42h  39353  cdlemeg46ngfr  39389  cdlemkid1  39793  lcfl7lem  40370  mapdpglem22  40564  mapdh6dN  40610  hdmap1l6d  40684  hdmapinvlem3  40791  lcmineqlem3  40896  selvvvval  41157  evlselv  41159  evlsmhpvvval  41167  nnadddir  41184  expgcd  41225  readdsub  41257  sn-negex12  41289  zmulcomlem  41328  prjspeclsp  41354  prjspner1  41368  3cubeslem3r  41425  diophin  41510  irrapxlem2  41561  pellexlem6  41572  pell1234qrmulcl  41593  rmxyval  41654  rmxyneg  41659  rmxyadd  41660  jm2.24  41702  jm2.25  41738  limexissupab  42033  omabs2  42082  tfsconcatrev  42098  naddwordnexlem4  42152  snhesn  42537  scottrankd  43007  radcnvrat  43073  binomcxplemnotnn0  43115  sub2times  43982  mul13d  43989  fperiodmullem  44013  fperiodmul  44014  isumneg  44318  climneg  44326  itgsinexp  44671  stoweidlem13  44729  stoweidlem42  44758  wallispilem4  44784  wallispilem5  44785  wallispi2lem1  44787  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem7  44796  stirlinglem10  44799  dirkertrigeqlem3  44816  fourierdlem30  44853  fourierdlem32  44855  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem83  44905  sqwvfoura  44944  sqwvfourb  44945  etransclem2  44952  etransclem46  44996  sharhght  45581  imasetpreimafvbijlemfv  46070  fmtnorec3  46216  quad1  46288  requad1  46290  isomgreqve  46493  ushrisomgr  46509  rngqiprngfulem4  46799  rngcid  46877  ringcid  46923  lmodvsmdi  47058  dmatALTbas  47082  ldepsprlem  47153  itcovalt2lem2lem2  47360  ackval3  47369  1subrec1sub  47391  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  itsclc0xyqsolr  47455  sinhpcosh  47785