Theorem 3eqtr2rd 2804

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  nneob  8626  xp1d2m1eqxm1d2  12475  negmod  13929  modeqmodmin  13954  faclbnd2  14304  cats1un  14734  cjmulval  15172  fsumsplit  15768  fzosump1  15779  bcxmas  15865  trireciplem  15892  geo2sum  15903  geo2lim  15905  geoisum1c  15910  mertenslem1  15914  fprodsplit  15996  risefallfac  16054  bpolydiflem  16084  eftlub  16141  tanadd  16199  addsin  16202  subsin  16203  subcos  16207  sadadd2lem2  16484  qredeu  16692  zsqrtelqelz  16793  4sqlem15  16995  rcaninv  17827  resssetc  18125  resscatc  18142  curfcl  18264  mulgaddcomlem  19139  conjghm  19289  gasubg  19342  dfod2  19604  efginvrel2  19767  efgcpbllemb  19795  odadd2  19889  frgpnabllem1  19913  srgbinomlem3  20278  pws1  20373  prdslmodd  21036  znunithash  21616  frlmipval  21831  frlmlbs  21849  psrlmod  22011  restcld  23232  clmneg  25143  rrxds  25455  itg2monolem1  25812  itgconst  25881  dvexp  26015  dvfsumabs  26085  dvtaylp  26433  taylthlem2  26437  tangtx  26570  logsqrt  26769  zrtelqelz  26823  lawcoslem1  26880  chordthmlem2  26898  chordthmlem4  26900  tanatan  26984  atanbndlem  26990  amgmlem  27054  basellem3  27147  basellem5  27149  mpodvdsmulf1o  27258  dvdsmulf1o  27260  chtub  27276  fsumvma  27277  lgsquad2lem1  27448  2sqlem8  27490  dchrmusum2  27558  logsqvma  27606  pntrlog2bndlem4  27644  pw2divsnegd  28542  miriso  28843  lmieu  28957  lnssplnglem  28998  ttgcontlem1  29085  brbtwn2  29106  ax5seglem1  29129  axcontlem2  29166  axcontlem4  29168  clwwlkel  30248  vc0  30777  hvsubdistr2  31253  adjlnop  32289  adjcoi  32303  cnvbraval  32313  fpwrelmap  32935  fsumiunle  33031  xrge0adddir  33196  cycpm2tr  33299  cycpmco2lem4  33309  cycpmco2lem7  33312  cyc3genpmlem  33331  archirngz  33369  archiabllem1b  33372  erler  33446  qusrn  33595  ressply10g  33763  ply1gsumz  33795  selvply1rhm0  33823  vietalem  33876  fedgmullem1  33926  fedgmullem2  33927  dimlssid  33929  constrrtcc  34032  rspectopn  34164  xrge0pluscn  34237  esumfzf  34366  esumiun  34391  volmeas  34528  omssubadd  34597  breprexplemc  34926  bnj553  35193  cvmliftlem6  35640  cvmliftlem10  35644  cvmlift2lem3  35655  finxpreclem4  37888  sin2h  38109  matunitlindflem2  38116  poimirlem16  38135  heibor  38320  ghomdiv  38391  3atlem1  40107  atmod3i2  40489  trljat2  40791  cdleme1  40851  cdleme22eALTN  40969  cdlemh2  41440  dihglblem3N  41919  dih1dimatlem0  41952  djhlsmcl  42038  mapdpglem30  42326  hdmapneg  42470  hgmapval1  42517  hgmapmul  42519  sn-1ne2  42880  sn-addrid  43030  fltnltalem  43244  3cubeslem3r  43268  3cubeslem4  43270  proot1ex  43773  tfsconcatfv  43918  dirkerper  46670  fourierdlem49  46729  fourierdlem83  46763  fourierdlem92  46772  sigarperm  47434  sigaradd  47440  cos5t  47473  fmtnorec1  48146  lincresunit3lem2  49102  itsclc0yqsollem1  49384  itsclinecirc0b  49396  fuco11bALT  49959  prstchomval  50180  sinhpcosh  50361  amgmwlem  50423