Theorem 3eqtr2rd 2779

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  nneob  8586  xp1d2m1eqxm1d2  12425  negmod  13872  modeqmodmin  13897  faclbnd2  14247  cats1un  14677  cjmulval  15101  fsumsplit  15697  fzosump1  15708  bcxmas  15794  trireciplem  15821  geo2sum  15832  geo2lim  15834  geoisum1c  15839  mertenslem1  15843  fprodsplit  15925  risefallfac  15983  bpolydiflem  16013  eftlub  16070  tanadd  16128  addsin  16131  subsin  16132  subcos  16136  sadadd2lem2  16413  qredeu  16621  zsqrtelqelz  16722  4sqlem15  16924  rcaninv  17755  resssetc  18053  resscatc  18070  curfcl  18192  mulgaddcomlem  19067  conjghm  19218  gasubg  19271  dfod2  19533  efginvrel2  19696  efgcpbllemb  19724  odadd2  19818  frgpnabllem1  19842  srgbinomlem3  20203  pws1  20298  prdslmodd  20958  znunithash  21557  frlmipval  21772  frlmlbs  21790  psrlmod  21951  restcld  23150  clmneg  25061  rrxds  25373  itg2monolem1  25730  itgconst  25799  dvexp  25933  dvfsumabs  26003  dvtaylp  26350  taylthlem2  26354  taylthlem2OLD  26355  tangtx  26485  logsqrt  26684  zrtelqelz  26738  lawcoslem1  26795  chordthmlem2  26813  chordthmlem4  26815  tanatan  26899  atanbndlem  26905  amgmlem  26970  basellem3  27063  basellem5  27065  mpodvdsmulf1o  27174  dvdsmulf1o  27176  chtub  27192  fsumvma  27193  lgsquad2lem1  27364  2sqlem8  27406  dchrmusum2  27474  logsqvma  27522  pntrlog2bndlem4  27560  pw2divsnegd  28458  miriso  28755  lmieu  28869  ttgcontlem1  28970  brbtwn2  28991  ax5seglem1  29014  axcontlem2  29051  axcontlem4  29053  clwwlkel  30134  vc0  30663  hvsubdistr2  31139  adjlnop  32175  adjcoi  32189  cnvbraval  32199  fpwrelmap  32824  fsumiunle  32920  xrge0adddir  33096  cycpm2tr  33198  cycpmco2lem4  33208  cycpmco2lem7  33211  cyc3genpmlem  33230  archirngz  33268  archiabllem1b  33271  erler  33344  qusrn  33487  ressply10g  33645  ply1gsumz  33677  vietalem  33741  fedgmullem1  33792  fedgmullem2  33793  dimlssid  33795  constrrtcc  33898  rspectopn  34030  xrge0pluscn  34103  esumfzf  34232  esumiun  34257  volmeas  34394  omssubadd  34463  breprexplemc  34795  bnj553  35059  cvmliftlem6  35491  cvmliftlem10  35495  cvmlift2lem3  35506  finxpreclem4  37727  sin2h  37948  matunitlindflem2  37955  poimirlem16  37974  heibor  38159  ghomdiv  38230  3atlem1  39946  atmod3i2  40328  trljat2  40630  cdleme1  40690  cdleme22eALTN  40808  cdlemh2  41279  dihglblem3N  41758  dih1dimatlem0  41791  djhlsmcl  41877  mapdpglem30  42165  hdmapneg  42309  hgmapval1  42356  hgmapmul  42358  sn-1ne2  42720  sn-addrid  42870  fltnltalem  43112  3cubeslem3r  43136  3cubeslem4  43138  proot1ex  43645  tfsconcatfv  43790  dirkerper  46545  fourierdlem83  46638  fourierdlem92  46647  sigarperm  47309  sigaradd  47315  fmtnorec1  48015  lincresunit3lem2  48971  itsclc0yqsollem1  49253  itsclinecirc0b  49265  fuco11bALT  49828  prstchomval  50049  sinhpcosh  50230  amgmwlem  50292