Theorem 3eqtr2d 2786

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  fmptapd  7205  negsub  11584  neg2sub  11596  divmuleq  11999  divneg2  12018  discr  14289  bcpasc  14370  hashgval2  14427  hashf1lem2  14505  relexpaddnn  15100  crim  15164  remullem  15177  isum1p  15889  geo2sum  15921  fallfacfwd  16084  fsumkthpow  16104  bpoly3  16106  bpoly4  16107  efi4p  16185  sinhval  16202  addcos  16222  cos2tsin  16227  demoivreALT  16249  rpnnen2lem11  16272  omeo  16414  pwp1fsum  16439  sadaddlem  16512  bitsres  16519  smumullem  16538  sqgcd  16609  expgcd  16610  eulerthlem2  16829  vfermltlALT  16849  pockthlem  16952  4sqlem10  16994  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  fuccocl  18034  resssetc  18159  resscatc  18176  uncfcurf  18309  yonedalem3b  18349  prdspjmhm  18864  grpinvid2  19032  imasgrp2  19095  mulgaddcomlem  19137  mulgmodid  19153  lagsubg2  19234  cntzsgrpcl  19374  cntzsubm  19378  sylow3lem2  19670  efgredleme  19785  ablsubsub  19859  ablsubsub4  19860  odadd2  19891  gex2abl  19893  pgpfac1lem3a  20120  pwspjmhmmgpd  20351  rngcid  20657  ringcid  20686  abvneg  20849  lmodfopne  20920  lsppr  21115  rngqiprngfulem4  21347  gzrngunit  21474  frlmsubgval  21808  frlmgsum  21815  psrass1  22007  resspsradd  22018  resspsrvsca  22020  mplcoe5  22081  mplmon2mul  22116  evlslem2  22126  evlsvarsrng  22146  coe1tm  22297  ply1scl1OLD  22318  ply1fermltlchr  22337  evls1varsrng  22365  mamuass  22427  mavmulass  22576  mulmarep1gsum2  22601  mdetuni0  22648  maducoeval2  22667  madulid  22672  mat2pmatmul  22758  decpmatmulsumfsupp  22800  pmatcollpwlem  22807  pm2mpmhmlem1  22845  cmpfi  23437  cnconn  23451  txrest  23660  utopsnneiplem  24277  blcvx  24839  tcphcphlem2  25289  cphipval2  25294  cphipval  25296  rrx0  25450  minveclem2  25479  pjthlem1  25490  uniioovol  25633  uniioombllem2  25637  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem5  25774  itg2mulc  25802  itg2monolem1  25805  itgaddlem1  25878  itgmulc2lem2  25888  dvrec  26013  lhop2  26074  ftc1lem5  26101  deg1submon1p  26212  plypf1  26271  coefv0  26307  coemulhi  26313  coemulc  26314  dgreq0  26325  dvply1  26343  vieta1  26372  aareccl  26386  aaliou3lem8  26405  dvtaylp  26430  mtest  26465  sineq0  26584  efif1olem2  26603  efif1olem4  26605  tanarg  26679  logtayl2  26722  nnlogbexp  26842  isosctrlem2  26880  chordthmlem2  26894  chordthmlem4  26896  heron  26899  dcubic1lem  26904  dcubic1  26906  mcubic  26908  dquart  26914  quart1lem  26916  quart1  26917  efiasin  26949  asinsin  26953  atancj  26971  efiatan  26973  atanlogaddlem  26974  cosatan  26982  atantan  26984  atans2  26992  log2cnv  27005  log2tlbnd  27006  birthdaylem2  27013  cxplim  27033  lgamgulmlem2  27091  wilthlem1  27129  basellem3  27144  musum  27252  musumsum  27253  muinv  27254  pclogsum  27277  mersenne  27289  dchrabs  27322  dchrinv  27323  lgseisenlem1  27437  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem1  27446  2lgslem1  27456  2sqmod  27498  chebbnd1lem3  27533  chpchtlim  27541  rplogsumlem2  27547  dchrisumlem2  27552  dchrmusum2  27556  mulog2sumlem1  27596  mulog2sumlem3  27598  vmalogdivsum2  27600  selberg4lem1  27622  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntibndlem2  27653  pntlemr  27664  pntlemf  27667  pntlemo  27669  addsdilem4  28198  mulsunif2lem  28213  halfcut  28434  zs12bday  28442  ragcom  28724  colperpexlem1  28756  lmiisolem  28822  hypcgrlem2  28826  trgcopyeulem  28831  brbtwn2  28938  colinearalglem1  28939  colinearalglem2  28940  axcontlem2  28998  axcontlem8  29004  numedglnl  29179  clwlkclwwlklem2a  30030  numclwlk1lem1  30401  numclwlk1lem2  30402  numclwwlk2  30413  grpoinvid2  30561  ablodivdiv4  30586  smcnlem  30729  ipidsq  30742  ipasslem2  30864  minvecolem2  30907  hv2times  31093  pjhthlem1  31423  pjds3i  31745  ho2times  31851  opsqrlem6  32177  pjclem4  32231  pj3si  32239  csmdsymi  32366  ofoprabco  32682  fcnvgreu  32691  quad3d  32757  swrdrndisj  32924  trsp2cyc  33116  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  rlocmulval  33241  imaslmod  33346  1arithufdlem3  33539  r1padd1  33593  frlmdim  33624  rrxdim  33627  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  extdg1id  33676  ccfldextdgrr  33682  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  qqhcn  33937  esumpr2  34031  esumpfinval  34039  esumpfinvalf  34040  carsggect  34283  oddpwdcv  34320  eulerpartlemgs2  34345  fibp1  34366  orvcelval  34433  ballotlemscr  34483  ballotlemfrci  34492  signsplypnf  34527  reprpmtf1o  34603  breprexplemc  34609  breprexp  34610  circlemeth  34617  lpadright  34661  revwlk  35092  subfacp1lem5  35152  cvmliftlem10  35262  circum  35642  faclimlem3  35707  fwddifnp1  36129  bj-bary1lem  37276  tan2h  37572  poimirlem3  37583  poimirlem13  37593  poimirlem14  37594  itgaddnclem1  37638  itgmulc2nclem2  37647  areacirclem1  37668  areacirclem4  37671  istotbnd3  37731  iscringd  37958  3atlem1  39440  pmod2iN  39806  polval2N  39863  lhple  39999  cdleme2  40185  cdleme35d  40409  cdleme42h  40439  cdlemeg46ngfr  40475  cdlemkid1  40879  lcfl7lem  41456  mapdpglem22  41650  mapdh6dN  41696  hdmap1l6d  41770  hdmapinvlem3  41877  lcmineqlem3  41988  nnadddir  42259  readdsub  42360  sn-negex12  42392  zmulcomlem  42431  selvvvval  42540  evlselv  42542  evlsmhpvvval  42550  prjspeclsp  42567  prjspner1  42581  3cubeslem3r  42643  diophin  42728  irrapxlem2  42779  pellexlem6  42790  pell1234qrmulcl  42811  rmxyval  42872  rmxyneg  42877  rmxyadd  42878  jm2.24  42920  jm2.25  42956  limexissupab  43245  omabs2  43294  tfsconcatrev  43310  naddwordnexlem4  43363  snhesn  43748  scottrankd  44217  radcnvrat  44283  binomcxplemnotnn0  44325  sub2times  45187  mul13d  45194  fperiodmullem  45218  fperiodmul  45219  isumneg  45523  climneg  45531  itgsinexp  45876  stoweidlem13  45934  stoweidlem42  45963  wallispilem4  45989  wallispilem5  45990  wallispi2lem1  45992  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  dirkertrigeqlem3  46021  fourierdlem30  46058  fourierdlem32  46060  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem83  46110  sqwvfoura  46149  sqwvfourb  46150  etransclem2  46157  etransclem46  46201  sharhght  46786  imasetpreimafvbijlemfv  47276  fmtnorec3  47422  quad1  47494  requad1  47496  ushggricedg  47780  lmodvsmdi  48107  dmatALTbas  48130  ldepsprlem  48201  itcovalt2lem2lem2  48408  ackval3  48417  1subrec1sub  48439  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  itsclc0xyqsolr  48503  sinhpcosh  48832