Theorem 3eqtr2d 2781

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  fmptapd  7122  negsub  11440  neg2sub  11452  divmuleq  11858  divneg2  11877  nnadddir  12231  discr  14200  bcpasc  14281  hashgval2  14338  hashf1lem2  14416  relexpaddnn  15011  crim  15075  remullem  15088  isum1p  15804  geo2sum  15836  fallfacfwd  15999  fsumkthpow  16019  bpoly3  16021  bpoly4  16022  efi4p  16102  sinhval  16119  addcos  16139  cos2tsin  16144  demoivreALT  16166  rpnnen2lem11  16189  omeo  16333  pwp1fsum  16358  sadaddlem  16433  bitsres  16440  smumullem  16459  sqgcd  16529  expgcd  16530  eulerthlem2  16750  vfermltlALT  16771  pockthlem  16874  4sqlem10  16916  vdwlem2  16951  vdwlem6  16955  vdwlem8  16957  fuccocl  17932  resssetc  18057  resscatc  18074  uncfcurf  18203  yonedalem3b  18243  prdspjmhm  18795  grpinvid2  18966  imasgrp2  19029  mulgaddcomlem  19071  mulgmodid  19087  lagsubg2  19167  cntzsgrpcl  19307  cntzsubm  19311  sylow3lem2  19601  efgredleme  19716  ablsubsub  19790  ablsubsub4  19791  odadd2  19822  gex2abl  19824  pgpfac1lem3a  20051  pwspjmhmmgpd  20305  rngcid  20614  ringcid  20643  abvneg  20805  lmodfopne  20897  lsppr  21090  rngqiprngfulem4  21314  gzrngunit  21415  frlmsubgval  21747  frlmgsum  21754  psrass1  21945  resspsradd  21956  resspsrvsca  21958  mplcoe5  22023  mplmon2mul  22052  evlslem2  22062  evlsvarsrng  22090  selvvvval  22125  coe1tm  22266  ply1fermltlchr  22305  evls1varsrng  22333  mamuass  22392  mavmulass  22539  mulmarep1gsum2  22564  mdetuni0  22611  maducoeval2  22630  madulid  22635  mat2pmatmul  22721  decpmatmulsumfsupp  22763  pmatcollpwlem  22770  pm2mpmhmlem1  22808  cmpfi  23398  cnconn  23412  txrest  23621  utopsnneiplem  24237  blcvx  24788  tcphcphlem2  25228  cphipval2  25233  cphipval  25235  rrx0  25389  minveclem2  25418  pjthlem1  25429  uniioovol  25571  uniioombllem2  25575  itg1addlem4  25691  mbfi1fseqlem5  25711  itg2mulc  25739  itg2monolem1  25742  itgaddlem1  25815  itgmulc2lem2  25825  dvrec  25947  lhop2  26007  ftc1lem5  26032  deg1submon1p  26143  plypf1  26202  coefv0  26238  coemulhi  26244  coemulc  26245  dgreq0  26255  dvply1  26275  vieta1  26303  aareccl  26317  aaliou3lem8  26336  dvtaylp  26360  mtest  26394  sineq0  26513  efif1olem2  26532  efif1olem4  26534  tanarg  26608  logtayl2  26651  nnlogbexp  26770  isosctrlem2  26808  chordthmlem2  26822  chordthmlem4  26824  heron  26827  dcubic1lem  26832  dcubic1  26834  mcubic  26836  dquart  26842  quart1lem  26844  quart1  26845  efiasin  26877  asinsin  26881  atancj  26899  efiatan  26901  atanlogaddlem  26902  cosatan  26910  atantan  26912  atans2  26920  log2cnv  26933  log2tlbnd  26934  birthdaylem2  26941  cxplim  26960  lgamgulmlem2  27018  wilthlem1  27056  basellem3  27071  musum  27179  musumsum  27180  muinv  27181  pclogsum  27203  mersenne  27215  dchrabs  27248  dchrinv  27249  lgseisenlem1  27363  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad2lem1  27372  2lgslem1  27382  2sqmod  27424  chebbnd1lem3  27459  chpchtlim  27467  rplogsumlem2  27473  dchrisumlem2  27478  dchrmusum2  27482  mulog2sumlem1  27522  mulog2sumlem3  27524  vmalogdivsum2  27526  selberg4lem1  27548  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntibndlem2  27579  pntlemr  27590  pntlemf  27593  pntlemo  27595  addsdilem4  28171  mulsunif2lem  28186  halfcut  28475  bdayfinbndlem1  28484  ragcom  28791  colperpexlem1  28823  lmiisolem  28889  hypcgrlem2  28893  trgcopyeulem  28898  brbtwn2  28999  colinearalglem1  29000  colinearalglem2  29001  axcontlem2  29059  axcontlem8  29065  numedglnl  29238  clwlkclwwlklem2a  30093  numclwlk1lem1  30464  numclwlk1lem2  30465  numclwwlk2  30476  grpoinvid2  30625  ablodivdiv4  30650  smcnlem  30793  ipidsq  30806  ipasslem2  30928  minvecolem2  30971  hv2times  31157  pjhthlem1  31487  pjds3i  31809  ho2times  31915  opsqrlem6  32241  pjclem4  32295  pj3si  32303  csmdsymi  32430  ofoprabco  32763  fcnvgreu  32771  quad3d  32848  nn0diffz0  32893  swrdrndisj  33043  trsp2cyc  33211  cycpmco2lem3  33216  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2  33221  conjga  33258  elrgspnlem1  33330  rlocmulval  33357  imaslmod  33443  1arithufdlem3  33636  deg1prod  33673  r1padd1  33698  selvply1rhmlem2  33712  mplvrpmrhm  33738  esplyfvaln  33765  frlmdim  33802  rrxdim  33805  lbsdiflsp0  33817  fedgmullem1  33820  fedgmullem2  33821  extdg1id  33857  ccfldextdgrr  33863  fldextrspunlem1  33866  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  constrrecl  33960  constrresqrtcl  33968  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  cos9thpiminplylem3  33975  cos9thpiminply  33979  qqhcn  34182  esumpr2  34258  esumpfinval  34266  esumpfinvalf  34267  carsggect  34509  oddpwdcv  34546  eulerpartlemgs2  34571  fibp1  34592  orvcelval  34660  ballotlemscr  34710  ballotlemfrci  34719  signsplypnf  34741  reprpmtf1o  34817  breprexplemc  34823  breprexp  34824  circlemeth  34831  lpadright  34875  revwlk  35360  subfacp1lem5  35419  cvmliftlem10  35529  circum  35909  faclimlem3  35980  fwddifnp1  36400  bj-bary1lem  37677  qdiff  37694  tan2h  37986  poimirlem3  37997  poimirlem13  38007  poimirlem14  38008  itgaddnclem1  38052  itgmulc2nclem2  38061  areacirclem1  38082  areacirclem4  38085  istotbnd3  38145  iscringd  38372  3atlem1  39982  pmod2iN  40348  polval2N  40405  lhple  40541  cdleme2  40727  cdleme35d  40951  cdleme42h  40981  cdlemeg46ngfr  41017  cdlemkid1  41421  lcfl7lem  41998  mapdpglem22  42192  mapdh6dN  42238  hdmap1l6d  42312  hdmapinvlem3  42419  lcmineqlem3  42523  readvrec2  42845  readdsub  42868  sn-negex12  42901  zmulcomlem  42964  evlselv  43046  evlsmhpvvval  43052  prjspeclsp  43069  prjspner1  43083  3cubeslem3r  43143  diophin  43228  irrapxlem2  43275  pellexlem6  43286  pell1234qrmulcl  43307  rmxyval  43367  rmxyneg  43372  rmxyadd  43373  jm2.24  43415  jm2.25  43451  limexissupab  43735  omabs2  43784  tfsconcatrev  43800  naddwordnexlem4  43853  snhesn  44237  scottrankd  44699  radcnvrat  44765  binomcxplemnotnn0  44807  sub2times  45728  mul13d  45735  fperiodmullem  45758  fperiodmul  45759  isumneg  46054  climneg  46062  itgsinexp  46405  stoweidlem13  46463  stoweidlem42  46492  wallispilem4  46518  wallispilem5  46519  wallispi2lem1  46521  stirlinglem1  46524  stirlinglem3  46526  stirlinglem4  46527  stirlinglem5  46528  stirlinglem7  46530  stirlinglem10  46533  dirkertrigeqlem3  46550  fourierdlem30  46587  fourierdlem32  46589  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem83  46639  sqwvfoura  46678  sqwvfourb  46679  etransclem2  46686  etransclem46  46730  sharhght  47315  sin3t  47341  sin5tlem1  47343  sin5tlem3  47345  cos5t  47349  imasetpreimafvbijlemfv  47884  fmtnorec3  48033  quad1  48118  requad1  48120  ushggricedg  48425  lmodvsmdi  48877  dmatALTbas  48899  ldepsprlem  48970  itcovalt2lem2lem2  49172  ackval3  49181  1subrec1sub  49203  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  itsclc0xyqsolr  49267  swapfid  49776  sinhpcosh  50237