Theorem 3eqtr2rd 2787

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  nneob  8712  xp1d2m1eqxm1d2  12547  negmod  13967  modeqmodmin  13992  faclbnd2  14340  cats1un  14769  cjmulval  15194  fsumsplit  15789  fzosump1  15800  bcxmas  15883  trireciplem  15910  geo2sum  15921  geo2lim  15923  geoisum1c  15928  mertenslem1  15932  fprodsplit  16014  risefallfac  16072  bpolydiflem  16102  eftlub  16157  tanadd  16215  addsin  16218  subsin  16219  subcos  16223  sadadd2lem2  16496  qredeu  16705  zsqrtelqelz  16805  4sqlem15  17006  rcaninv  17855  resssetc  18159  resscatc  18176  estrreslem1OLD  18206  curfcl  18302  mulgaddcomlem  19137  conjghm  19289  gasubg  19342  dfod2  19606  efginvrel2  19769  efgcpbllemb  19797  odadd2  19891  frgpnabllem1  19915  srgbinomlem3  20255  pws1  20348  prdslmodd  20990  znunithash  21606  frlmipval  21822  frlmlbs  21840  psrlmod  22003  restcld  23201  clmneg  25133  rrxds  25446  itg2monolem1  25805  itgconst  25874  dvexp  26011  dvfsumabs  26083  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  tangtx  26565  logsqrt  26764  zrtelqelz  26819  lawcoslem1  26876  chordthmlem2  26894  chordthmlem4  26896  tanatan  26980  atanbndlem  26986  amgmlem  27051  basellem3  27144  basellem5  27146  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chtub  27274  fsumvma  27275  lgsquad2lem1  27446  2sqlem8  27488  dchrmusum2  27556  logsqvma  27604  pntrlog2bndlem4  27642  miriso  28696  lmieu  28810  ttgcontlem1  28917  brbtwn2  28938  ax5seglem1  28961  axcontlem2  28998  axcontlem4  29000  clwwlkel  30078  vc0  30606  hvsubdistr2  31082  adjlnop  32118  adjcoi  32132  cnvbraval  32142  fpwrelmap  32747  fsumiunle  32833  xrge0adddir  33004  cycpm2tr  33112  cycpmco2lem4  33122  cycpmco2lem7  33125  cyc3genpmlem  33144  archirngz  33169  archiabllem1b  33172  erler  33237  qusrn  33402  ressply10g  33557  ply1gsumz  33584  fedgmullem1  33642  fedgmullem2  33643  dimlssid  33645  constrrtcc  33726  rspectopn  33813  xrge0pluscn  33886  esumfzf  34033  esumiun  34058  volmeas  34195  omssubadd  34265  breprexplemc  34609  bnj553  34874  cvmliftlem6  35258  cvmliftlem10  35262  cvmlift2lem3  35273  finxpreclem4  37360  sin2h  37570  matunitlindflem2  37577  poimirlem16  37596  heibor  37781  ghomdiv  37852  3atlem1  39440  atmod3i2  39822  trljat2  40124  cdleme1  40184  cdleme22eALTN  40302  cdlemh2  40773  dihglblem3N  41252  dih1dimatlem0  41285  djhlsmcl  41371  mapdpglem30  41659  hdmapneg  41803  hgmapval1  41850  hgmapmul  41852  sn-1ne2  42254  sn-addrid  42396  fltnltalem  42617  3cubeslem3r  42643  3cubeslem4  42645  proot1ex  43157  tfsconcatfv  43303  dirkerper  46017  fourierdlem83  46110  fourierdlem92  46119  sigarperm  46781  sigaradd  46787  fmtnorec1  47411  lincresunit3lem2  48209  itsclc0yqsollem1  48496  itsclinecirc0b  48508  prstchomval  48741  sinhpcosh  48832  amgmwlem  48896