MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr2rd Structured version   Visualization version   GIF version

Theorem 3eqtr2rd 2784
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
StepHypRef Expression
1 3eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr2d.2 . . 3 (𝜑𝐶 = 𝐵)
31, 2eqtr4d 2780 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2778 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  nneob  8603  xp1d2m1eqxm1d2  12408  negmod  13822  modeqmodmin  13847  faclbnd2  14192  cats1un  14610  cjmulval  15031  fsumsplit  15627  fzosump1  15638  bcxmas  15721  trireciplem  15748  geo2sum  15759  geo2lim  15761  geoisum1c  15766  mertenslem1  15770  fprodsplit  15850  risefallfac  15908  bpolydiflem  15938  eftlub  15992  tanadd  16050  addsin  16053  subsin  16054  subcos  16058  sadadd2lem2  16331  qredeu  16535  zsqrtelqelz  16634  4sqlem15  16832  rcaninv  17678  resssetc  17979  resscatc  17996  estrreslem1OLD  18026  curfcl  18122  mulgaddcomlem  18900  conjghm  19040  gasubg  19083  dfod2  19347  efginvrel2  19510  efgcpbllemb  19538  odadd2  19628  frgpnabllem1  19652  srgbinomlem3  19960  pws1  20041  prdslmodd  20433  znunithash  20974  frlmipval  21188  frlmlbs  21206  psrlmod  21373  restcld  22526  clmneg  24447  rrxds  24760  itg2monolem1  25118  itgconst  25186  dvexp  25320  dvfsumabs  25390  dvtaylp  25732  taylthlem2  25736  tangtx  25865  logsqrt  26062  lawcoslem1  26168  chordthmlem2  26186  chordthmlem4  26188  tanatan  26272  atanbndlem  26278  amgmlem  26342  basellem3  26435  basellem5  26437  dvdsmulf1o  26546  chtub  26563  fsumvma  26564  lgsquad2lem1  26735  2sqlem8  26777  dchrmusum2  26845  logsqvma  26893  pntrlog2bndlem4  26931  miriso  27615  lmieu  27729  ttgcontlem1  27836  brbtwn2  27857  ax5seglem1  27880  axcontlem2  27917  axcontlem4  27919  clwwlkel  28993  vc0  29519  hvsubdistr2  29995  adjlnop  31031  adjcoi  31045  cnvbraval  31055  fpwrelmap  31653  fsumiunle  31728  xrge0adddir  31886  cycpm2tr  31971  cycpmco2lem4  31981  cycpmco2lem7  31984  cyc3genpmlem  32003  archirngz  32028  archiabllem1b  32031  ressply10g  32280  fedgmullem1  32327  fedgmullem2  32328  rspectopn  32451  xrge0pluscn  32524  esumfzf  32671  esumiun  32696  volmeas  32833  omssubadd  32903  breprexplemc  33248  bnj553  33513  cvmliftlem6  33887  cvmliftlem10  33891  cvmlift2lem3  33902  finxpreclem4  35868  sin2h  36071  matunitlindflem2  36078  poimirlem16  36097  heibor  36283  ghomdiv  36354  3atlem1  37949  atmod3i2  38331  trljat2  38633  cdleme1  38693  cdleme22eALTN  38811  cdlemh2  39282  dihglblem3N  39761  dih1dimatlem0  39794  djhlsmcl  39880  mapdpglem30  40168  hdmapneg  40312  hgmapval1  40359  hgmapmul  40361  sn-1ne2  40784  zrtelqelz  40834  sn-addid1  40892  fltnltalem  41003  3cubeslem3r  41013  3cubeslem4  41015  proot1ex  41531  dirkerper  44344  fourierdlem83  44437  fourierdlem92  44446  sigarperm  45108  sigaradd  45114  fmtnorec1  45736  lincresunit3lem2  46568  itsclc0yqsollem1  46855  itsclinecirc0b  46867  prstchomval  47101  sinhpcosh  47192  amgmwlem  47256
  Copyright terms: Public domain W3C validator