Theorem 3eqtr2rd 2778

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

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

This theorem is referenced by:  nneob  8673  xp1d2m1eqxm1d2  12500  negmod  13939  modeqmodmin  13964  faclbnd2  14314  cats1un  14744  cjmulval  15169  fsumsplit  15762  fzosump1  15773  bcxmas  15856  trireciplem  15883  geo2sum  15894  geo2lim  15896  geoisum1c  15901  mertenslem1  15905  fprodsplit  15987  risefallfac  16045  bpolydiflem  16075  eftlub  16132  tanadd  16190  addsin  16193  subsin  16194  subcos  16198  sadadd2lem2  16474  qredeu  16682  zsqrtelqelz  16782  4sqlem15  16984  rcaninv  17812  resssetc  18110  resscatc  18127  curfcl  18249  mulgaddcomlem  19085  conjghm  19237  gasubg  19290  dfod2  19550  efginvrel2  19713  efgcpbllemb  19741  odadd2  19835  frgpnabllem1  19859  srgbinomlem3  20193  pws1  20290  prdslmodd  20931  znunithash  21530  frlmipval  21744  frlmlbs  21762  psrlmod  21925  restcld  23115  clmneg  25037  rrxds  25350  itg2monolem1  25708  itgconst  25777  dvexp  25914  dvfsumabs  25986  dvtaylp  26335  taylthlem2  26339  taylthlem2OLD  26340  tangtx  26471  logsqrt  26670  zrtelqelz  26725  lawcoslem1  26782  chordthmlem2  26800  chordthmlem4  26802  tanatan  26886  atanbndlem  26892  amgmlem  26957  basellem3  27050  basellem5  27052  mpodvdsmulf1o  27161  dvdsmulf1o  27163  chtub  27180  fsumvma  27181  lgsquad2lem1  27352  2sqlem8  27394  dchrmusum2  27462  logsqvma  27510  pntrlog2bndlem4  27548  pw2divsnegd  28389  miriso  28654  lmieu  28768  ttgcontlem1  28869  brbtwn2  28889  ax5seglem1  28912  axcontlem2  28949  axcontlem4  28951  clwwlkel  30032  vc0  30560  hvsubdistr2  31036  adjlnop  32072  adjcoi  32086  cnvbraval  32096  fpwrelmap  32715  fsumiunle  32813  xrge0adddir  33018  cycpm2tr  33135  cycpmco2lem4  33145  cycpmco2lem7  33148  cyc3genpmlem  33167  archirngz  33192  archiabllem1b  33195  erler  33265  qusrn  33429  ressply10g  33585  ply1gsumz  33613  fedgmullem1  33674  fedgmullem2  33675  dimlssid  33677  constrrtcc  33774  rspectopn  33903  xrge0pluscn  33976  esumfzf  34105  esumiun  34130  volmeas  34267  omssubadd  34337  breprexplemc  34669  bnj553  34934  cvmliftlem6  35317  cvmliftlem10  35321  cvmlift2lem3  35332  finxpreclem4  37417  sin2h  37639  matunitlindflem2  37646  poimirlem16  37665  heibor  37850  ghomdiv  37921  3atlem1  39507  atmod3i2  39889  trljat2  40191  cdleme1  40251  cdleme22eALTN  40369  cdlemh2  40840  dihglblem3N  41319  dih1dimatlem0  41352  djhlsmcl  41438  mapdpglem30  41726  hdmapneg  41870  hgmapval1  41917  hgmapmul  41919  sn-1ne2  42283  sn-addrid  42438  fltnltalem  42660  3cubeslem3r  42685  3cubeslem4  42687  proot1ex  43195  tfsconcatfv  43340  dirkerper  46105  fourierdlem83  46198  fourierdlem92  46207  sigarperm  46869  sigaradd  46875  fmtnorec1  47531  lincresunit3lem2  48436  itsclc0yqsollem1  48722  itsclinecirc0b  48734  fuco11bALT  49229  prstchomval  49416  sinhpcosh  49584  amgmwlem  49646