Theorem 3eqtr2d 2784

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 2781	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtrd 2778	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  fmptapd  7025  negsub  11199  neg2sub  11211  divmuleq  11610  divneg2  11629  discr  13883  bcpasc  13963  hashgval2  14021  hashf1lem2  14098  relexpaddnn  14690  crim  14754  remullem  14767  isum1p  15481  geo2sum  15513  fallfacfwd  15674  fsumkthpow  15694  bpoly3  15696  bpoly4  15697  efi4p  15774  sinhval  15791  addcos  15811  cos2tsin  15816  demoivreALT  15838  rpnnen2lem11  15861  omeo  16003  pwp1fsum  16028  sadaddlem  16101  bitsres  16108  smumullem  16127  sqgcd  16198  eulerthlem2  16411  vfermltlALT  16431  pockthlem  16534  4sqlem10  16576  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  fuccocl  17598  resssetc  17723  resscatc  17740  uncfcurf  17873  yonedalem3b  17913  prdspjmhm  18382  grpinvid2  18546  imasgrp2  18605  mulgaddcomlem  18641  mulgmodid  18657  lagsubg2  18732  cntzsubm  18857  sylow3lem2  19148  efgredleme  19264  ablsubsub  19334  ablsubsub4  19335  odadd2  19365  gex2abl  19367  pgpfac1lem3a  19594  abvneg  20009  lmodfopne  20076  lsppr  20270  gzrngunit  20576  frlmsubgval  20882  frlmgsum  20889  psrass1  21084  resspsradd  21095  resspsrvsca  21097  mplcoe5  21151  mplmon2mul  21187  evlslem2  21199  evlsvarsrng  21219  coe1tm  21354  ply1scl1  21373  evls1varsrng  21416  mamuass  21459  mavmulass  21606  mulmarep1gsum2  21631  mdetuni0  21678  maducoeval2  21697  madulid  21702  mat2pmatmul  21788  decpmatmulsumfsupp  21830  pmatcollpwlem  21837  pm2mpmhmlem1  21875  cmpfi  22467  cnconn  22481  txrest  22690  utopsnneiplem  23307  blcvx  23867  tcphcphlem2  24305  cphipval2  24310  cphipval  24312  rrx0  24466  minveclem2  24495  pjthlem1  24506  uniioovol  24648  uniioombllem2  24652  itg1addlem4  24768  itg1addlem4OLD  24769  mbfi1fseqlem5  24789  itg2mulc  24817  itg2monolem1  24820  itgaddlem1  24892  itgmulc2lem2  24902  dvrec  25024  lhop2  25084  ftc1lem5  25109  deg1submon1p  25222  plypf1  25278  coefv0  25314  coemulhi  25320  coemulc  25321  dgreq0  25331  dvply1  25349  vieta1  25377  aareccl  25391  aaliou3lem8  25410  dvtaylp  25434  mtest  25468  sineq0  25585  efif1olem2  25604  efif1olem4  25606  tanarg  25679  logtayl2  25722  nnlogbexp  25836  isosctrlem2  25874  chordthmlem2  25888  chordthmlem4  25890  heron  25893  dcubic1lem  25898  dcubic1  25900  mcubic  25902  dquart  25908  quart1lem  25910  quart1  25911  efiasin  25943  asinsin  25947  atancj  25965  efiatan  25967  atanlogaddlem  25968  cosatan  25976  atantan  25978  atans2  25986  log2cnv  25999  log2tlbnd  26000  birthdaylem2  26007  cxplim  26026  lgamgulmlem2  26084  wilthlem1  26122  basellem3  26137  musum  26245  musumsum  26246  muinv  26247  pclogsum  26268  mersenne  26280  dchrabs  26313  dchrinv  26314  lgseisenlem1  26428  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem1  26437  2lgslem1  26447  2sqmod  26489  chebbnd1lem3  26524  chpchtlim  26532  rplogsumlem2  26538  dchrisumlem2  26543  dchrmusum2  26547  mulog2sumlem1  26587  mulog2sumlem3  26589  vmalogdivsum2  26591  selberg4lem1  26613  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntibndlem2  26644  pntlemr  26655  pntlemf  26658  pntlemo  26660  ragcom  26963  colperpexlem1  26995  lmiisolem  27061  hypcgrlem2  27065  trgcopyeulem  27070  brbtwn2  27176  colinearalglem1  27177  colinearalglem2  27178  axcontlem2  27236  axcontlem8  27242  numedglnl  27417  clwlkclwwlklem2a  28263  numclwlk1lem1  28634  numclwlk1lem2  28635  numclwwlk2  28646  grpoinvid2  28792  ablodivdiv4  28817  smcnlem  28960  ipidsq  28973  ipasslem2  29095  minvecolem2  29138  hv2times  29324  pjhthlem1  29654  pjds3i  29976  ho2times  30082  opsqrlem6  30408  pjclem4  30462  pj3si  30470  csmdsymi  30597  ofoprabco  30903  fcnvgreu  30912  swrdrndisj  31131  trsp2cyc  31292  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2  31302  imaslmod  31455  ply1fermltl  31572  frlmdim  31596  rrxdim  31599  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  extdg1id  31640  ccfldextdgrr  31644  qqhcn  31841  esumpr2  31935  esumpfinval  31943  esumpfinvalf  31944  carsggect  32185  oddpwdcv  32222  eulerpartlemgs2  32247  fibp1  32268  orvcelval  32335  ballotlemscr  32385  ballotlemfrci  32394  signsplypnf  32429  reprpmtf1o  32506  breprexplemc  32512  breprexp  32513  circlemeth  32520  lpadright  32564  revwlk  32986  subfacp1lem5  33046  cvmliftlem10  33156  circum  33532  faclimlem3  33617  fwddifnp1  34394  bj-bary1lem  35408  tan2h  35696  poimirlem3  35707  poimirlem13  35717  poimirlem14  35718  itgaddnclem1  35762  itgmulc2nclem2  35771  areacirclem1  35792  areacirclem4  35795  istotbnd3  35856  iscringd  36083  3atlem1  37424  pmod2iN  37790  polval2N  37847  lhple  37983  cdleme2  38169  cdleme35d  38393  cdleme42h  38423  cdlemeg46ngfr  38459  cdlemkid1  38863  lcfl7lem  39440  mapdpglem22  39634  mapdh6dN  39680  hdmap1l6d  39754  hdmapinvlem3  39861  lcmineqlem3  39967  pwspjmhmmgpd  40192  nnadddir  40221  expgcd  40255  readdsub  40288  sn-negex12  40319  prjspeclsp  40372  prjspner1  40384  3cubeslem3r  40425  diophin  40510  irrapxlem2  40561  pellexlem6  40572  pell1234qrmulcl  40593  rmxyval  40653  rmxyneg  40658  rmxyadd  40659  jm2.24  40701  jm2.25  40737  snhesn  41283  scottrankd  41755  radcnvrat  41821  binomcxplemnotnn0  41863  sub2times  42702  mul13d  42707  fperiodmullem  42732  fperiodmul  42733  isumneg  43033  climneg  43041  itgsinexp  43386  stoweidlem13  43444  stoweidlem42  43473  wallispilem4  43499  wallispilem5  43500  wallispi2lem1  43502  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem7  43511  stirlinglem10  43514  dirkertrigeqlem3  43531  fourierdlem30  43568  fourierdlem32  43570  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem83  43620  sqwvfoura  43659  sqwvfourb  43660  etransclem2  43667  etransclem46  43711  sharhght  44268  imasetpreimafvbijlemfv  44742  fmtnorec3  44888  quad1  44960  requad1  44962  isomgreqve  45165  ushrisomgr  45181  rngcid  45425  ringcid  45471  lmodvsmdi  45606  dmatALTbas  45630  ldepsprlem  45701  itcovalt2lem2lem2  45908  ackval3  45917  1subrec1sub  45939  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  itsclc0xyqsolr  46003  sinhpcosh  46328