Theorem 3eqtr2rd 2807

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  nneob  8648  xp1d2m1eqxm1d2  12515  negmod  13972  modeqmodmin  13997  faclbnd2  14347  cats1un  14782  cjmulval  15222  fsumsplit  15817  fzosump1  15828  bcxmas  15914  trireciplem  15941  geo2sum  15952  geo2lim  15954  geoisum1c  15959  mertenslem1  15963  fprodsplit  16045  risefallfac  16103  bpolydiflem  16132  eftlub  16189  tanadd  16247  addsin  16250  subsin  16251  subcos  16255  sadadd2lem2  16532  qredeu  16740  zsqrtelqelz  16841  4sqlem15  17043  rcaninv  17875  resssetc  18173  resscatc  18190  curfcl  18312  mulgaddcomlem  19209  conjghm  19365  gasubg  19418  dfod2  19680  efginvrel2  19843  efgcpbllemb  19871  odadd2  19965  frgpnabllem1  19989  srgbinomlem3  20356  pws1  20454  prdslmodd  21142  znunithash  21766  frlmipval  21981  frlmlbs  21999  psrlmod  22161  restcld  23381  clmneg  25293  rrxds  25605  itg2monolem1  25962  itgconst  26031  dvexp  26165  dvfsumabs  26235  dvtaylp  26586  taylthlem2  26590  tangtx  26723  logsqrt  26922  zrtelqelz  26976  lawcoslem1  27033  chordthmlem2  27051  chordthmlem4  27053  tanatan  27137  atanbndlem  27143  amgmlem  27207  basellem3  27300  basellem5  27302  mpodvdsmulf1o  27411  dvdsmulf1o  27413  chtub  27429  fsumvma  27430  lgsquad2lem1  27601  2sqlem8  27643  dchrmusum2  27711  logsqvma  27759  pntrlog2bndlem4  27797  pw2divsnegd  28695  miriso  29000  lnssplnglem  29126  lmieu  29146  ttgcontlem1  29291  brbtwn2  29312  ax5seglem1  29335  axcontlem2  29372  axcontlem4  29374  clwwlkel  30466  vc0  30999  hvsubdistr2  31475  adjlnop  32511  adjcoi  32525  cnvbraval  32535  fpwrelmap  33150  fsumiunle  33245  xrge0adddir  33404  cycpm2tr  33505  cycpmco2lem4  33515  cycpmco2lem7  33518  cyc3genpmlem  33537  archirngz  33575  archiabllem1b  33578  erler  33651  qusrn  33784  ressply10g  33923  ply1gsumz  33955  selvply1rhm0  33982  vietalem  34035  fedgmullem1  34085  fedgmullem2  34086  dimlssid  34088  constrrtcc  34191  rspectopn  34323  xrge0pluscn  34396  esumfzf  34525  esumiun  34550  volmeas  34688  omssubadd  34757  breprexplemc  35086  bnj553  35353  cvmliftlem6  35821  cvmliftlem10  35825  cvmlift2lem3  35836  finxpreclem4  38099  sin2h  38320  matunitlindflem2  38327  poimirlem16  38346  heibor  38532  ghomdiv  38603  3atlem1  40317  atmod3i2  40699  trljat2  41001  cdleme1  41061  cdleme22eALTN  41179  cdlemh2  41650  dihglblem3N  42129  dih1dimatlem0  42162  djhlsmcl  42248  mapdpglem30  42536  hdmapneg  42680  hgmapval1  42727  hgmapmul  42729  sn-1ne2  43092  sn-addrid  43242  fltnltalem  43454  3cubeslem3r  43478  3cubeslem4  43480  proot1ex  43983  tfsconcatfv  44128  dirkerper  46870  fourierdlem49  46929  fourierdlem83  46963  fourierdlem92  46972  sigarperm  47634  sigaradd  47640  cos5t  47676  fmtnorec1  48349  lincresunit3lem2  49319  itsclc0yqsollem1  49601  itsclinecirc0b  49613  fuco11bALT  50175  prstchomval  50396  sinhpcosh  50577  amgmwlem  50709