Theorem 3eqtr2rd 2776

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
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2772	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2770	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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  nneob  8677  xp1d2m1eqxm1d2  12504  negmod  13940  modeqmodmin  13965  faclbnd2  14313  cats1un  14742  cjmulval  15167  fsumsplit  15760  fzosump1  15771  bcxmas  15854  trireciplem  15881  geo2sum  15892  geo2lim  15894  geoisum1c  15899  mertenslem1  15903  fprodsplit  15985  risefallfac  16043  bpolydiflem  16073  eftlub  16128  tanadd  16186  addsin  16189  subsin  16190  subcos  16194  sadadd2lem2  16470  qredeu  16678  zsqrtelqelz  16778  4sqlem15  16980  rcaninv  17814  resssetc  18113  resscatc  18130  curfcl  18252  mulgaddcomlem  19089  conjghm  19241  gasubg  19294  dfod2  19555  efginvrel2  19718  efgcpbllemb  19746  odadd2  19840  frgpnabllem1  19864  srgbinomlem3  20198  pws1  20295  prdslmodd  20940  znunithash  21550  frlmipval  21766  frlmlbs  21784  psrlmod  21947  restcld  23145  clmneg  25069  rrxds  25382  itg2monolem1  25740  itgconst  25809  dvexp  25946  dvfsumabs  26018  dvtaylp  26367  taylthlem2  26371  taylthlem2OLD  26372  tangtx  26502  logsqrt  26701  zrtelqelz  26756  lawcoslem1  26813  chordthmlem2  26831  chordthmlem4  26833  tanatan  26917  atanbndlem  26923  amgmlem  26988  basellem3  27081  basellem5  27083  mpodvdsmulf1o  27192  dvdsmulf1o  27194  chtub  27211  fsumvma  27212  lgsquad2lem1  27383  2sqlem8  27425  dchrmusum2  27493  logsqvma  27541  pntrlog2bndlem4  27579  miriso  28633  lmieu  28747  ttgcontlem1  28849  brbtwn2  28869  ax5seglem1  28892  axcontlem2  28929  axcontlem4  28931  clwwlkel  30012  vc0  30540  hvsubdistr2  31016  adjlnop  32052  adjcoi  32066  cnvbraval  32076  fpwrelmap  32691  fsumiunle  32778  xrge0adddir  32969  cycpm2tr  33085  cycpmco2lem4  33095  cycpmco2lem7  33098  cyc3genpmlem  33117  archirngz  33142  archiabllem1b  33145  erler  33215  qusrn  33378  ressply10g  33533  ply1gsumz  33560  fedgmullem1  33621  fedgmullem2  33622  dimlssid  33624  constrrtcc  33717  rspectopn  33807  xrge0pluscn  33880  esumfzf  34011  esumiun  34036  volmeas  34173  omssubadd  34243  breprexplemc  34588  bnj553  34853  cvmliftlem6  35236  cvmliftlem10  35240  cvmlift2lem3  35251  finxpreclem4  37336  sin2h  37558  matunitlindflem2  37565  poimirlem16  37584  heibor  37769  ghomdiv  37840  3atlem1  39426  atmod3i2  39808  trljat2  40110  cdleme1  40170  cdleme22eALTN  40288  cdlemh2  40759  dihglblem3N  41238  dih1dimatlem0  41271  djhlsmcl  41357  mapdpglem30  41645  hdmapneg  41789  hgmapval1  41836  hgmapmul  41838  sn-1ne2  42245  sn-addrid  42395  fltnltalem  42617  3cubeslem3r  42643  3cubeslem4  42645  proot1ex  43153  tfsconcatfv  43299  dirkerper  46056  fourierdlem83  46149  fourierdlem92  46158  sigarperm  46820  sigaradd  46826  fmtnorec1  47470  lincresunit3lem2  48343  itsclc0yqsollem1  48629  itsclinecirc0b  48641  fuco11bALT  48997  prstchomval  49152  sinhpcosh  49255  amgmwlem  49317