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  8574  xp1d2m1eqxm1d2  12378  negmod  13823  modeqmodmin  13848  faclbnd2  14198  cats1un  14627  cjmulval  15052  fsumsplit  15648  fzosump1  15659  bcxmas  15742  trireciplem  15769  geo2sum  15780  geo2lim  15782  geoisum1c  15787  mertenslem1  15791  fprodsplit  15873  risefallfac  15931  bpolydiflem  15961  eftlub  16018  tanadd  16076  addsin  16079  subsin  16080  subcos  16084  sadadd2lem2  16361  qredeu  16569  zsqrtelqelz  16669  4sqlem15  16871  rcaninv  17701  resssetc  17999  resscatc  18016  curfcl  18138  mulgaddcomlem  18976  conjghm  19128  gasubg  19181  dfod2  19443  efginvrel2  19606  efgcpbllemb  19634  odadd2  19728  frgpnabllem1  19752  srgbinomlem3  20113  pws1  20210  prdslmodd  20872  znunithash  21471  frlmipval  21686  frlmlbs  21704  psrlmod  21867  restcld  23057  clmneg  24979  rrxds  25291  itg2monolem1  25649  itgconst  25718  dvexp  25855  dvfsumabs  25927  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  tangtx  26412  logsqrt  26611  zrtelqelz  26666  lawcoslem1  26723  chordthmlem2  26741  chordthmlem4  26743  tanatan  26827  atanbndlem  26833  amgmlem  26898  basellem3  26991  basellem5  26993  mpodvdsmulf1o  27102  dvdsmulf1o  27104  chtub  27121  fsumvma  27122  lgsquad2lem1  27293  2sqlem8  27335  dchrmusum2  27403  logsqvma  27451  pntrlog2bndlem4  27489  pw2divsnegd  28341  miriso  28615  lmieu  28729  ttgcontlem1  28830  brbtwn2  28850  ax5seglem1  28873  axcontlem2  28910  axcontlem4  28912  clwwlkel  29990  vc0  30518  hvsubdistr2  30994  adjlnop  32030  adjcoi  32044  cnvbraval  32054  fpwrelmap  32676  fsumiunle  32774  xrge0adddir  32972  cycpm2tr  33061  cycpmco2lem4  33071  cycpmco2lem7  33074  cyc3genpmlem  33093  archirngz  33131  archiabllem1b  33134  erler  33205  qusrn  33346  ressply10g  33502  ply1gsumz  33531  fedgmullem1  33596  fedgmullem2  33597  dimlssid  33599  constrrtcc  33702  rspectopn  33834  xrge0pluscn  33907  esumfzf  34036  esumiun  34061  volmeas  34198  omssubadd  34268  breprexplemc  34600  bnj553  34865  cvmliftlem6  35267  cvmliftlem10  35271  cvmlift2lem3  35282  finxpreclem4  37372  sin2h  37594  matunitlindflem2  37601  poimirlem16  37620  heibor  37805  ghomdiv  37876  3atlem1  39466  atmod3i2  39848  trljat2  40150  cdleme1  40210  cdleme22eALTN  40328  cdlemh2  40799  dihglblem3N  41278  dih1dimatlem0  41311  djhlsmcl  41397  mapdpglem30  41685  hdmapneg  41829  hgmapval1  41876  hgmapmul  41878  sn-1ne2  42242  sn-addrid  42398  fltnltalem  42639  3cubeslem3r  42664  3cubeslem4  42666  proot1ex  43173  tfsconcatfv  43318  dirkerper  46081  fourierdlem83  46174  fourierdlem92  46183  sigarperm  46845  sigaradd  46851  fmtnorec1  47525  lincresunit3lem2  48469  itsclc0yqsollem1  48751  itsclinecirc0b  48763  fuco11bALT  49327  prstchomval  49548  sinhpcosh  49729  amgmwlem  49791