Theorem 3eqtr2d 2785

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

Syntax hints:   → wi 4   = wceq 1539

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  fmptapd  7052  negsub  11278  neg2sub  11290  divmuleq  11689  divneg2  11708  discr  13964  bcpasc  14044  hashgval2  14102  hashf1lem2  14179  relexpaddnn  14771  crim  14835  remullem  14848  isum1p  15562  geo2sum  15594  fallfacfwd  15755  fsumkthpow  15775  bpoly3  15777  bpoly4  15778  efi4p  15855  sinhval  15872  addcos  15892  cos2tsin  15897  demoivreALT  15919  rpnnen2lem11  15942  omeo  16084  pwp1fsum  16109  sadaddlem  16182  bitsres  16189  smumullem  16208  sqgcd  16279  eulerthlem2  16492  vfermltlALT  16512  pockthlem  16615  4sqlem10  16657  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  fuccocl  17691  resssetc  17816  resscatc  17833  uncfcurf  17966  yonedalem3b  18006  prdspjmhm  18476  grpinvid2  18640  imasgrp2  18699  mulgaddcomlem  18735  mulgmodid  18751  lagsubg2  18826  cntzsubm  18951  sylow3lem2  19242  efgredleme  19358  ablsubsub  19428  ablsubsub4  19429  odadd2  19459  gex2abl  19461  pgpfac1lem3a  19688  abvneg  20103  lmodfopne  20170  lsppr  20364  gzrngunit  20673  frlmsubgval  20981  frlmgsum  20988  psrass1  21183  resspsradd  21194  resspsrvsca  21196  mplcoe5  21250  mplmon2mul  21286  evlslem2  21298  evlsvarsrng  21318  coe1tm  21453  ply1scl1  21472  evls1varsrng  21515  mamuass  21558  mavmulass  21707  mulmarep1gsum2  21732  mdetuni0  21779  maducoeval2  21798  madulid  21803  mat2pmatmul  21889  decpmatmulsumfsupp  21931  pmatcollpwlem  21938  pm2mpmhmlem1  21976  cmpfi  22568  cnconn  22582  txrest  22791  utopsnneiplem  23408  blcvx  23970  tcphcphlem2  24409  cphipval2  24414  cphipval  24416  rrx0  24570  minveclem2  24599  pjthlem1  24610  uniioovol  24752  uniioombllem2  24756  itg1addlem4  24872  itg1addlem4OLD  24873  mbfi1fseqlem5  24893  itg2mulc  24921  itg2monolem1  24924  itgaddlem1  24996  itgmulc2lem2  25006  dvrec  25128  lhop2  25188  ftc1lem5  25213  deg1submon1p  25326  plypf1  25382  coefv0  25418  coemulhi  25424  coemulc  25425  dgreq0  25435  dvply1  25453  vieta1  25481  aareccl  25495  aaliou3lem8  25514  dvtaylp  25538  mtest  25572  sineq0  25689  efif1olem2  25708  efif1olem4  25710  tanarg  25783  logtayl2  25826  nnlogbexp  25940  isosctrlem2  25978  chordthmlem2  25992  chordthmlem4  25994  heron  25997  dcubic1lem  26002  dcubic1  26004  mcubic  26006  dquart  26012  quart1lem  26014  quart1  26015  efiasin  26047  asinsin  26051  atancj  26069  efiatan  26071  atanlogaddlem  26072  cosatan  26080  atantan  26082  atans2  26090  log2cnv  26103  log2tlbnd  26104  birthdaylem2  26111  cxplim  26130  lgamgulmlem2  26188  wilthlem1  26226  basellem3  26241  musum  26349  musumsum  26350  muinv  26351  pclogsum  26372  mersenne  26384  dchrabs  26417  dchrinv  26418  lgseisenlem1  26532  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2lem1  26541  2lgslem1  26551  2sqmod  26593  chebbnd1lem3  26628  chpchtlim  26636  rplogsumlem2  26642  dchrisumlem2  26647  dchrmusum2  26651  mulog2sumlem1  26691  mulog2sumlem3  26693  vmalogdivsum2  26695  selberg4lem1  26717  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntibndlem2  26748  pntlemr  26759  pntlemf  26762  pntlemo  26764  ragcom  27068  colperpexlem1  27100  lmiisolem  27166  hypcgrlem2  27170  trgcopyeulem  27175  brbtwn2  27282  colinearalglem1  27283  colinearalglem2  27284  axcontlem2  27342  axcontlem8  27348  numedglnl  27523  clwlkclwwlklem2a  28371  numclwlk1lem1  28742  numclwlk1lem2  28743  numclwwlk2  28754  grpoinvid2  28900  ablodivdiv4  28925  smcnlem  29068  ipidsq  29081  ipasslem2  29203  minvecolem2  29246  hv2times  29432  pjhthlem1  29762  pjds3i  30084  ho2times  30190  opsqrlem6  30516  pjclem4  30570  pj3si  30578  csmdsymi  30705  ofoprabco  31010  fcnvgreu  31019  swrdrndisj  31238  trsp2cyc  31399  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2  31409  imaslmod  31562  ply1fermltl  31679  frlmdim  31703  rrxdim  31706  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  extdg1id  31747  ccfldextdgrr  31751  qqhcn  31950  esumpr2  32044  esumpfinval  32052  esumpfinvalf  32053  carsggect  32294  oddpwdcv  32331  eulerpartlemgs2  32356  fibp1  32377  orvcelval  32444  ballotlemscr  32494  ballotlemfrci  32503  signsplypnf  32538  reprpmtf1o  32615  breprexplemc  32621  breprexp  32622  circlemeth  32629  lpadright  32673  revwlk  33095  subfacp1lem5  33155  cvmliftlem10  33265  circum  33641  faclimlem3  33720  fwddifnp1  34476  bj-bary1lem  35490  tan2h  35778  poimirlem3  35789  poimirlem13  35799  poimirlem14  35800  itgaddnclem1  35844  itgmulc2nclem2  35853  areacirclem1  35874  areacirclem4  35877  istotbnd3  35938  iscringd  36165  3atlem1  37504  pmod2iN  37870  polval2N  37927  lhple  38063  cdleme2  38249  cdleme35d  38473  cdleme42h  38503  cdlemeg46ngfr  38539  cdlemkid1  38943  lcfl7lem  39520  mapdpglem22  39714  mapdh6dN  39760  hdmap1l6d  39834  hdmapinvlem3  39941  lcmineqlem3  40046  pwspjmhmmgpd  40274  nnadddir  40307  expgcd  40341  readdsub  40374  sn-negex12  40405  prjspeclsp  40458  prjspner1  40470  3cubeslem3r  40516  diophin  40601  irrapxlem2  40652  pellexlem6  40663  pell1234qrmulcl  40684  rmxyval  40744  rmxyneg  40749  rmxyadd  40750  jm2.24  40792  jm2.25  40828  snhesn  41401  scottrankd  41873  radcnvrat  41939  binomcxplemnotnn0  41981  sub2times  42820  mul13d  42825  fperiodmullem  42849  fperiodmul  42850  isumneg  43150  climneg  43158  itgsinexp  43503  stoweidlem13  43561  stoweidlem42  43590  wallispilem4  43616  wallispilem5  43617  wallispi2lem1  43619  stirlinglem1  43622  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem7  43628  stirlinglem10  43631  dirkertrigeqlem3  43648  fourierdlem30  43685  fourierdlem32  43687  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem83  43737  sqwvfoura  43776  sqwvfourb  43777  etransclem2  43784  etransclem46  43828  sharhght  44392  imasetpreimafvbijlemfv  44865  fmtnorec3  45011  quad1  45083  requad1  45085  isomgreqve  45288  ushrisomgr  45304  rngcid  45548  ringcid  45594  lmodvsmdi  45729  dmatALTbas  45753  ldepsprlem  45824  itcovalt2lem2lem2  46031  ackval3  46040  1subrec1sub  46062  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  itsclc0xyqsolr  46126  sinhpcosh  46453