Theorem 3eqtr2rd 2785

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 2781	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2779	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  nneob  8446  xp1d2m1eqxm1d2  12157  negmod  13564  modeqmodmin  13589  faclbnd2  13933  cats1un  14362  cjmulval  14784  fsumsplit  15381  fzosump1  15392  bcxmas  15475  trireciplem  15502  geo2sum  15513  geo2lim  15515  geoisum1c  15520  mertenslem1  15524  fprodsplit  15604  risefallfac  15662  bpolydiflem  15692  eftlub  15746  tanadd  15804  addsin  15807  subsin  15808  subcos  15812  sadadd2lem2  16085  qredeu  16291  zsqrtelqelz  16390  4sqlem15  16588  rcaninv  17423  resssetc  17723  resscatc  17740  estrreslem1OLD  17770  curfcl  17866  mulgaddcomlem  18641  conjghm  18780  gasubg  18823  dfod2  19086  efginvrel2  19248  efgcpbllemb  19276  odadd2  19365  frgpnabllem1  19389  srgbinomlem3  19693  pws1  19770  prdslmodd  20146  znunithash  20684  frlmipval  20896  frlmlbs  20914  psrlmod  21080  restcld  22231  clmneg  24150  rrxds  24462  itg2monolem1  24820  itgconst  24888  dvexp  25022  dvfsumabs  25092  dvtaylp  25434  taylthlem2  25438  tangtx  25567  logsqrt  25764  lawcoslem1  25870  chordthmlem2  25888  chordthmlem4  25890  tanatan  25974  atanbndlem  25980  amgmlem  26044  basellem3  26137  basellem5  26139  dvdsmulf1o  26248  chtub  26265  fsumvma  26266  lgsquad2lem1  26437  2sqlem8  26479  dchrmusum2  26547  logsqvma  26595  pntrlog2bndlem4  26633  miriso  26935  lmieu  27049  ttgcontlem1  27155  brbtwn2  27176  ax5seglem1  27199  axcontlem2  27236  axcontlem4  27238  clwwlkel  28311  vc0  28837  hvsubdistr2  29313  adjlnop  30349  adjcoi  30363  cnvbraval  30373  fpwrelmap  30970  fsumiunle  31045  xrge0adddir  31203  cycpm2tr  31288  cycpmco2lem4  31298  cycpmco2lem7  31301  cyc3genpmlem  31320  archirngz  31345  archiabllem1b  31348  fedgmullem1  31612  fedgmullem2  31613  rspectopn  31719  xrge0pluscn  31792  esumfzf  31937  esumiun  31962  volmeas  32099  omssubadd  32167  breprexplemc  32512  bnj553  32778  cvmliftlem6  33152  cvmliftlem10  33156  cvmlift2lem3  33167  finxpreclem4  35492  sin2h  35694  matunitlindflem2  35701  poimirlem16  35720  heibor  35906  ghomdiv  35977  3atlem1  37424  atmod3i2  37806  trljat2  38108  cdleme1  38168  cdleme22eALTN  38286  cdlemh2  38757  dihglblem3N  39236  dih1dimatlem0  39269  djhlsmcl  39355  mapdpglem30  39643  hdmapneg  39787  hgmapval1  39834  hgmapmul  39836  sn-1ne2  40216  zrtelqelz  40266  sn-addid1  40323  fltnltalem  40415  3cubeslem3r  40425  3cubeslem4  40427  proot1ex  40942  dirkerper  43527  fourierdlem83  43620  fourierdlem92  43629  sigarperm  44263  sigaradd  44269  fmtnorec1  44877  lincresunit3lem2  45709  itsclc0yqsollem1  45996  itsclinecirc0b  46008  prstchomval  46241  sinhpcosh  46328  amgmwlem  46392