Theorem 3eqtr2rd 2771

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 2767	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2765	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  nneob  8597  xp1d2m1eqxm1d2  12412  negmod  13857  modeqmodmin  13882  faclbnd2  14232  cats1un  14662  cjmulval  15087  fsumsplit  15683  fzosump1  15694  bcxmas  15777  trireciplem  15804  geo2sum  15815  geo2lim  15817  geoisum1c  15822  mertenslem1  15826  fprodsplit  15908  risefallfac  15966  bpolydiflem  15996  eftlub  16053  tanadd  16111  addsin  16114  subsin  16115  subcos  16119  sadadd2lem2  16396  qredeu  16604  zsqrtelqelz  16704  4sqlem15  16906  rcaninv  17736  resssetc  18034  resscatc  18051  curfcl  18173  mulgaddcomlem  19011  conjghm  19163  gasubg  19216  dfod2  19478  efginvrel2  19641  efgcpbllemb  19669  odadd2  19763  frgpnabllem1  19787  srgbinomlem3  20148  pws1  20245  prdslmodd  20907  znunithash  21506  frlmipval  21721  frlmlbs  21739  psrlmod  21902  restcld  23092  clmneg  25014  rrxds  25326  itg2monolem1  25684  itgconst  25753  dvexp  25890  dvfsumabs  25962  dvtaylp  26311  taylthlem2  26315  taylthlem2OLD  26316  tangtx  26447  logsqrt  26646  zrtelqelz  26701  lawcoslem1  26758  chordthmlem2  26776  chordthmlem4  26778  tanatan  26862  atanbndlem  26868  amgmlem  26933  basellem3  27026  basellem5  27028  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chtub  27156  fsumvma  27157  lgsquad2lem1  27328  2sqlem8  27370  dchrmusum2  27438  logsqvma  27486  pntrlog2bndlem4  27524  pw2divsnegd  28376  miriso  28650  lmieu  28764  ttgcontlem1  28865  brbtwn2  28885  ax5seglem1  28908  axcontlem2  28945  axcontlem4  28947  clwwlkel  30025  vc0  30553  hvsubdistr2  31029  adjlnop  32065  adjcoi  32079  cnvbraval  32089  fpwrelmap  32706  fsumiunle  32804  xrge0adddir  33002  cycpm2tr  33091  cycpmco2lem4  33101  cycpmco2lem7  33104  cyc3genpmlem  33123  archirngz  33158  archiabllem1b  33161  erler  33232  qusrn  33373  ressply10g  33529  ply1gsumz  33557  fedgmullem1  33618  fedgmullem2  33619  dimlssid  33621  constrrtcc  33718  rspectopn  33850  xrge0pluscn  33923  esumfzf  34052  esumiun  34077  volmeas  34214  omssubadd  34284  breprexplemc  34616  bnj553  34881  cvmliftlem6  35270  cvmliftlem10  35274  cvmlift2lem3  35285  finxpreclem4  37375  sin2h  37597  matunitlindflem2  37604  poimirlem16  37623  heibor  37808  ghomdiv  37879  3atlem1  39470  atmod3i2  39852  trljat2  40154  cdleme1  40214  cdleme22eALTN  40332  cdlemh2  40803  dihglblem3N  41282  dih1dimatlem0  41315  djhlsmcl  41401  mapdpglem30  41689  hdmapneg  41833  hgmapval1  41880  hgmapmul  41882  sn-1ne2  42246  sn-addrid  42402  fltnltalem  42643  3cubeslem3r  42668  3cubeslem4  42670  proot1ex  43178  tfsconcatfv  43323  dirkerper  46087  fourierdlem83  46180  fourierdlem92  46189  sigarperm  46851  sigaradd  46857  fmtnorec1  47531  lincresunit3lem2  48462  itsclc0yqsollem1  48744  itsclinecirc0b  48756  fuco11bALT  49320  prstchomval  49541  sinhpcosh  49722  amgmwlem  49784