Theorem 3eqtr2d 2782

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

Syntax hints:   → wi 4   = wceq 1540

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728

This theorem is referenced by:  fmptapd  7093  negsub  11362  neg2sub  11374  divmuleq  11773  divneg2  11792  discr  14048  bcpasc  14128  hashgval2  14185  hashf1lem2  14262  relexpaddnn  14853  crim  14917  remullem  14930  isum1p  15644  geo2sum  15676  fallfacfwd  15837  fsumkthpow  15857  bpoly3  15859  bpoly4  15860  efi4p  15937  sinhval  15954  addcos  15974  cos2tsin  15979  demoivreALT  16001  rpnnen2lem11  16024  omeo  16166  pwp1fsum  16191  sadaddlem  16264  bitsres  16271  smumullem  16290  sqgcd  16359  eulerthlem2  16572  vfermltlALT  16592  pockthlem  16695  4sqlem10  16737  vdwlem2  16772  vdwlem6  16776  vdwlem8  16778  fuccocl  17771  resssetc  17896  resscatc  17913  uncfcurf  18046  yonedalem3b  18086  prdspjmhm  18556  grpinvid2  18719  imasgrp2  18778  mulgaddcomlem  18814  mulgmodid  18830  lagsubg2  18905  cntzsubm  19030  sylow3lem2  19321  efgredleme  19436  ablsubsub  19506  ablsubsub4  19507  odadd2  19537  gex2abl  19539  pgpfac1lem3a  19766  abvneg  20192  lmodfopne  20259  lsppr  20453  gzrngunit  20762  frlmsubgval  21070  frlmgsum  21077  psrass1  21272  resspsradd  21283  resspsrvsca  21285  mplcoe5  21339  mplmon2mul  21375  evlslem2  21387  evlsvarsrng  21407  coe1tm  21542  ply1scl1  21561  evls1varsrng  21604  mamuass  21647  mavmulass  21796  mulmarep1gsum2  21821  mdetuni0  21868  maducoeval2  21887  madulid  21892  mat2pmatmul  21978  decpmatmulsumfsupp  22020  pmatcollpwlem  22027  pm2mpmhmlem1  22065  cmpfi  22657  cnconn  22671  txrest  22880  utopsnneiplem  23497  blcvx  24059  tcphcphlem2  24498  cphipval2  24503  cphipval  24505  rrx0  24659  minveclem2  24688  pjthlem1  24699  uniioovol  24841  uniioombllem2  24845  itg1addlem4  24961  itg1addlem4OLD  24962  mbfi1fseqlem5  24982  itg2mulc  25010  itg2monolem1  25013  itgaddlem1  25085  itgmulc2lem2  25095  dvrec  25217  lhop2  25277  ftc1lem5  25302  deg1submon1p  25415  plypf1  25471  coefv0  25507  coemulhi  25513  coemulc  25514  dgreq0  25524  dvply1  25542  vieta1  25570  aareccl  25584  aaliou3lem8  25603  dvtaylp  25627  mtest  25661  sineq0  25778  efif1olem2  25797  efif1olem4  25799  tanarg  25872  logtayl2  25915  nnlogbexp  26029  isosctrlem2  26067  chordthmlem2  26081  chordthmlem4  26083  heron  26086  dcubic1lem  26091  dcubic1  26093  mcubic  26095  dquart  26101  quart1lem  26103  quart1  26104  efiasin  26136  asinsin  26140  atancj  26158  efiatan  26160  atanlogaddlem  26161  cosatan  26169  atantan  26171  atans2  26179  log2cnv  26192  log2tlbnd  26193  birthdaylem2  26200  cxplim  26219  lgamgulmlem2  26277  wilthlem1  26315  basellem3  26330  musum  26438  musumsum  26439  muinv  26440  pclogsum  26461  mersenne  26473  dchrabs  26506  dchrinv  26507  lgseisenlem1  26621  lgsquadlem1  26626  lgsquadlem2  26627  lgsquadlem3  26628  lgsquad2lem1  26630  2lgslem1  26640  2sqmod  26682  chebbnd1lem3  26717  chpchtlim  26725  rplogsumlem2  26731  dchrisumlem2  26736  dchrmusum2  26740  mulog2sumlem1  26780  mulog2sumlem3  26782  vmalogdivsum2  26784  selberg4lem1  26806  pntrlog2bndlem2  26824  pntrlog2bndlem4  26826  pntibndlem2  26837  pntlemr  26848  pntlemf  26851  pntlemo  26853  ragcom  27289  colperpexlem1  27321  lmiisolem  27387  hypcgrlem2  27391  trgcopyeulem  27396  brbtwn2  27503  colinearalglem1  27504  colinearalglem2  27505  axcontlem2  27563  axcontlem8  27569  numedglnl  27744  clwlkclwwlklem2a  28591  numclwlk1lem1  28962  numclwlk1lem2  28963  numclwwlk2  28974  grpoinvid2  29120  ablodivdiv4  29145  smcnlem  29288  ipidsq  29301  ipasslem2  29423  minvecolem2  29466  hv2times  29652  pjhthlem1  29982  pjds3i  30304  ho2times  30410  opsqrlem6  30736  pjclem4  30790  pj3si  30798  csmdsymi  30925  ofoprabco  31229  fcnvgreu  31238  swrdrndisj  31457  trsp2cyc  31618  cycpmco2lem3  31623  cycpmco2lem4  31624  cycpmco2lem5  31625  cycpmco2lem6  31626  cycpmco2  31628  imaslmod  31790  ply1fermltlchr  31908  frlmdim  31933  rrxdim  31936  lbsdiflsp0  31946  fedgmullem1  31949  fedgmullem2  31950  extdg1id  31977  ccfldextdgrr  31981  qqhcn  32180  esumpr2  32274  esumpfinval  32282  esumpfinvalf  32283  carsggect  32526  oddpwdcv  32563  eulerpartlemgs2  32588  fibp1  32609  orvcelval  32676  ballotlemscr  32726  ballotlemfrci  32735  signsplypnf  32770  reprpmtf1o  32847  breprexplemc  32853  breprexp  32854  circlemeth  32861  lpadright  32905  revwlk  33326  subfacp1lem5  33386  cvmliftlem10  33496  circum  33872  faclimlem3  33945  fwddifnp1  34558  bj-bary1lem  35579  tan2h  35867  poimirlem3  35878  poimirlem13  35888  poimirlem14  35889  itgaddnclem1  35933  itgmulc2nclem2  35942  areacirclem1  35963  areacirclem4  35966  istotbnd3  36027  iscringd  36254  3atlem1  37744  pmod2iN  38110  polval2N  38167  lhple  38303  cdleme2  38489  cdleme35d  38713  cdleme42h  38743  cdlemeg46ngfr  38779  cdlemkid1  39183  lcfl7lem  39760  mapdpglem22  39954  mapdh6dN  40000  hdmap1l6d  40074  hdmapinvlem3  40181  lcmineqlem3  40286  pwspjmhmmgpd  40517  nnadddir  40550  expgcd  40584  readdsub  40617  sn-negex12  40648  prjspeclsp  40701  prjspner1  40713  3cubeslem3r  40759  diophin  40844  irrapxlem2  40895  pellexlem6  40906  pell1234qrmulcl  40927  rmxyval  40988  rmxyneg  40993  rmxyadd  40994  jm2.24  41036  jm2.25  41072  omabs2  41305  snhesn  41704  scottrankd  42176  radcnvrat  42242  binomcxplemnotnn0  42284  sub2times  43137  mul13d  43142  fperiodmullem  43166  fperiodmul  43167  isumneg  43468  climneg  43476  itgsinexp  43821  stoweidlem13  43879  stoweidlem42  43908  wallispilem4  43934  wallispilem5  43935  wallispi2lem1  43937  stirlinglem1  43940  stirlinglem3  43942  stirlinglem4  43943  stirlinglem5  43944  stirlinglem7  43946  stirlinglem10  43949  dirkertrigeqlem3  43966  fourierdlem30  44003  fourierdlem32  44005  fourierdlem42  44015  fourierdlem48  44020  fourierdlem49  44021  fourierdlem83  44055  sqwvfoura  44094  sqwvfourb  44095  etransclem2  44102  etransclem46  44146  sharhght  44721  imasetpreimafvbijlemfv  45194  fmtnorec3  45340  quad1  45412  requad1  45414  isomgreqve  45617  ushrisomgr  45633  rngcid  45877  ringcid  45923  lmodvsmdi  46058  dmatALTbas  46082  ldepsprlem  46153  itcovalt2lem2lem2  46360  ackval3  46369  1subrec1sub  46391  eenglngeehlnmlem1  46423  eenglngeehlnmlem2  46424  itsclc0xyqsolr  46455  sinhpcosh  46782