Theorem 3eqtr2d 2772

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 2769	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2766	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 2121  ax-ext 2703

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

This theorem is referenced by:  fmptapd  7100  negsub  11404  neg2sub  11416  divmuleq  11821  divneg2  11840  discr  14142  bcpasc  14223  hashgval2  14280  hashf1lem2  14358  relexpaddnn  14953  crim  15017  remullem  15030  isum1p  15743  geo2sum  15775  fallfacfwd  15938  fsumkthpow  15958  bpoly3  15960  bpoly4  15961  efi4p  16041  sinhval  16058  addcos  16078  cos2tsin  16083  demoivreALT  16105  rpnnen2lem11  16128  omeo  16272  pwp1fsum  16297  sadaddlem  16372  bitsres  16379  smumullem  16398  sqgcd  16468  expgcd  16469  eulerthlem2  16688  vfermltlALT  16709  pockthlem  16812  4sqlem10  16854  vdwlem2  16889  vdwlem6  16893  vdwlem8  16895  fuccocl  17869  resssetc  17994  resscatc  18011  uncfcurf  18140  yonedalem3b  18180  prdspjmhm  18732  grpinvid2  18900  imasgrp2  18963  mulgaddcomlem  19005  mulgmodid  19021  lagsubg2  19101  cntzsgrpcl  19241  cntzsubm  19245  sylow3lem2  19535  efgredleme  19650  ablsubsub  19724  ablsubsub4  19725  odadd2  19756  gex2abl  19758  pgpfac1lem3a  19985  pwspjmhmmgpd  20241  rngcid  20545  ringcid  20574  abvneg  20736  lmodfopne  20828  lsppr  21022  rngqiprngfulem4  21246  gzrngunit  21365  frlmsubgval  21697  frlmgsum  21704  psrass1  21896  resspsradd  21907  resspsrvsca  21909  mplcoe5  21970  mplmon2mul  21999  evlslem2  22009  evlsvarsrng  22029  coe1tm  22182  ply1scl1OLD  22203  ply1fermltlchr  22222  evls1varsrng  22250  mamuass  22312  mavmulass  22459  mulmarep1gsum2  22484  mdetuni0  22531  maducoeval2  22550  madulid  22555  mat2pmatmul  22641  decpmatmulsumfsupp  22683  pmatcollpwlem  22690  pm2mpmhmlem1  22728  cmpfi  23318  cnconn  23332  txrest  23541  utopsnneiplem  24157  blcvx  24708  tcphcphlem2  25158  cphipval2  25163  cphipval  25165  rrx0  25319  minveclem2  25348  pjthlem1  25359  uniioovol  25502  uniioombllem2  25506  itg1addlem4  25622  mbfi1fseqlem5  25642  itg2mulc  25670  itg2monolem1  25673  itgaddlem1  25746  itgmulc2lem2  25756  dvrec  25881  lhop2  25942  ftc1lem5  25969  deg1submon1p  26080  plypf1  26139  coefv0  26175  coemulhi  26181  coemulc  26182  dgreq0  26193  dvply1  26213  vieta1  26242  aareccl  26256  aaliou3lem8  26275  dvtaylp  26300  mtest  26335  sineq0  26455  efif1olem2  26474  efif1olem4  26476  tanarg  26550  logtayl2  26593  nnlogbexp  26713  isosctrlem2  26751  chordthmlem2  26765  chordthmlem4  26767  heron  26770  dcubic1lem  26775  dcubic1  26777  mcubic  26779  dquart  26785  quart1lem  26787  quart1  26788  efiasin  26820  asinsin  26824  atancj  26842  efiatan  26844  atanlogaddlem  26845  cosatan  26853  atantan  26855  atans2  26863  log2cnv  26876  log2tlbnd  26877  birthdaylem2  26884  cxplim  26904  lgamgulmlem2  26962  wilthlem1  27000  basellem3  27015  musum  27123  musumsum  27124  muinv  27125  pclogsum  27148  mersenne  27160  dchrabs  27193  dchrinv  27194  lgseisenlem1  27308  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  lgsquad2lem1  27317  2lgslem1  27327  2sqmod  27369  chebbnd1lem3  27404  chpchtlim  27412  rplogsumlem2  27418  dchrisumlem2  27423  dchrmusum2  27427  mulog2sumlem1  27467  mulog2sumlem3  27469  vmalogdivsum2  27471  selberg4lem1  27493  pntrlog2bndlem2  27511  pntrlog2bndlem4  27513  pntibndlem2  27524  pntlemr  27535  pntlemf  27538  pntlemo  27540  addsdilem4  28088  mulsunif2lem  28103  halfcut  28373  zs12bday  28389  ragcom  28671  colperpexlem1  28703  lmiisolem  28769  hypcgrlem2  28773  trgcopyeulem  28778  brbtwn2  28878  colinearalglem1  28879  colinearalglem2  28880  axcontlem2  28938  axcontlem8  28944  numedglnl  29117  clwlkclwwlklem2a  29970  numclwlk1lem1  30341  numclwlk1lem2  30342  numclwwlk2  30353  grpoinvid2  30501  ablodivdiv4  30526  smcnlem  30669  ipidsq  30682  ipasslem2  30804  minvecolem2  30847  hv2times  31033  pjhthlem1  31363  pjds3i  31685  ho2times  31791  opsqrlem6  32117  pjclem4  32171  pj3si  32179  csmdsymi  32306  ofoprabco  32638  fcnvgreu  32647  quad3d  32725  swrdrndisj  32930  trsp2cyc  33084  cycpmco2lem3  33089  cycpmco2lem4  33090  cycpmco2lem5  33091  cycpmco2lem6  33092  cycpmco2  33094  conjga  33131  elrgspnlem1  33201  rlocmulval  33228  imaslmod  33310  1arithufdlem3  33503  r1padd1  33560  mplvrpmrhm  33569  frlmdim  33616  rrxdim  33619  lbsdiflsp0  33631  fedgmullem1  33634  fedgmullem2  33635  extdg1id  33671  ccfldextdgrr  33677  fldextrspunlem1  33680  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrrecl  33774  constrresqrtcl  33782  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  cos9thpiminplylem3  33789  cos9thpiminply  33793  qqhcn  33996  esumpr2  34072  esumpfinval  34080  esumpfinvalf  34081  carsggect  34323  oddpwdcv  34360  eulerpartlemgs2  34385  fibp1  34406  orvcelval  34474  ballotlemscr  34524  ballotlemfrci  34533  signsplypnf  34555  reprpmtf1o  34631  breprexplemc  34637  breprexp  34638  circlemeth  34645  lpadright  34689  revwlk  35161  subfacp1lem5  35220  cvmliftlem10  35330  circum  35710  faclimlem3  35781  fwddifnp1  36199  bj-bary1lem  37344  tan2h  37652  poimirlem3  37663  poimirlem13  37673  poimirlem14  37674  itgaddnclem1  37718  itgmulc2nclem2  37727  areacirclem1  37748  areacirclem4  37751  istotbnd3  37811  iscringd  38038  3atlem1  39522  pmod2iN  39888  polval2N  39945  lhple  40081  cdleme2  40267  cdleme35d  40491  cdleme42h  40521  cdlemeg46ngfr  40557  cdlemkid1  40961  lcfl7lem  41538  mapdpglem22  41732  mapdh6dN  41778  hdmap1l6d  41852  hdmapinvlem3  41959  lcmineqlem3  42064  nnadddir  42303  readvrec2  42394  readdsub  42417  sn-negex12  42450  zmulcomlem  42500  selvvvval  42618  evlselv  42620  evlsmhpvvval  42628  prjspeclsp  42645  prjspner1  42659  3cubeslem3r  42720  diophin  42805  irrapxlem2  42856  pellexlem6  42867  pell1234qrmulcl  42888  rmxyval  42948  rmxyneg  42953  rmxyadd  42954  jm2.24  42996  jm2.25  43032  limexissupab  43316  omabs2  43365  tfsconcatrev  43381  naddwordnexlem4  43434  snhesn  43819  scottrankd  44281  radcnvrat  44347  binomcxplemnotnn0  44389  sub2times  45314  mul13d  45321  fperiodmullem  45344  fperiodmul  45345  isumneg  45642  climneg  45650  itgsinexp  45993  stoweidlem13  46051  stoweidlem42  46080  wallispilem4  46106  wallispilem5  46107  wallispi2lem1  46109  stirlinglem1  46112  stirlinglem3  46114  stirlinglem4  46115  stirlinglem5  46116  stirlinglem7  46118  stirlinglem10  46121  dirkertrigeqlem3  46138  fourierdlem30  46175  fourierdlem32  46177  fourierdlem42  46187  fourierdlem48  46192  fourierdlem49  46193  fourierdlem83  46227  sqwvfoura  46266  sqwvfourb  46267  etransclem2  46274  etransclem46  46318  sharhght  46903  imasetpreimafvbijlemfv  47433  fmtnorec3  47579  quad1  47651  requad1  47653  ushggricedg  47958  lmodvsmdi  48410  dmatALTbas  48433  ldepsprlem  48504  itcovalt2lem2lem2  48706  ackval3  48715  1subrec1sub  48737  eenglngeehlnmlem1  48769  eenglngeehlnmlem2  48770  itsclc0xyqsolr  48801  swapfid  49311  sinhpcosh  49772