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

Theorem 3eqtr2rd 2860
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 2856 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2854 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  nneob  8268  xp1d2m1eqxm1d2  11879  negmod  13272  modeqmodmin  13297  faclbnd2  13639  cats1un  14071  cjmulval  14492  fsumsplit  15085  fzosump1  15095  bcxmas  15178  trireciplem  15205  geo2sum  15217  geo2lim  15219  geoisum1c  15224  mertenslem1  15228  fprodsplit  15308  risefallfac  15366  bpolydiflem  15396  eftlub  15450  tanadd  15508  addsin  15511  subsin  15512  subcos  15516  sadadd2lem2  15787  qredeu  15990  zsqrtelqelz  16086  4sqlem15  16283  rcaninv  17052  resssetc  17340  resscatc  17353  estrreslem1  17375  curfcl  17470  mulgaddcomlem  18188  conjghm  18327  gasubg  18370  dfod2  18620  efginvrel2  18782  efgcpbllemb  18810  odadd2  18898  frgpnabllem1  18922  srgbinomlem3  19221  pws1  19295  prdslmodd  19670  psrlmod  20109  znunithash  20639  frlmipval  20851  frlmlbs  20869  restcld  21708  clmneg  23612  rrxds  23923  itg2monolem1  24278  itgconst  24346  dvexp  24477  dvfsumabs  24547  dvtaylp  24885  taylthlem2  24889  tangtx  25018  logsqrt  25214  lawcoslem1  25320  chordthmlem2  25338  chordthmlem4  25340  tanatan  25424  atanbndlem  25430  amgmlem  25494  basellem3  25587  basellem5  25589  dvdsmulf1o  25698  chtub  25715  fsumvma  25716  lgsquad2lem1  25887  2sqlem8  25929  dchrmusum2  25997  logsqvma  26045  pntrlog2bndlem4  26083  miriso  26383  lmieu  26497  ttgcontlem1  26598  brbtwn2  26618  ax5seglem1  26641  axcontlem2  26678  axcontlem4  26680  clwwlkel  27752  vc0  28278  hvsubdistr2  28754  adjlnop  29790  adjcoi  29804  cnvbraval  29814  fpwrelmap  30395  fsumiunle  30472  xrge0adddir  30606  cycpm2tr  30688  cycpmco2lem4  30698  cycpmco2lem7  30701  cyc3genpmlem  30720  archirngz  30745  archiabllem1b  30748  fedgmullem1  30924  fedgmullem2  30925  xrge0pluscn  31082  esumfzf  31227  esumiun  31252  volmeas  31389  omssubadd  31457  breprexplemc  31802  bnj553  32069  cvmliftlem6  32434  cvmliftlem10  32438  cvmlift2lem3  32449  finxpreclem4  34557  sin2h  34763  matunitlindflem2  34770  poimirlem16  34789  heibor  34980  ghomdiv  35051  3atlem1  36499  atmod3i2  36881  trljat2  37183  cdleme1  37243  cdleme22eALTN  37361  cdlemh2  37832  dihglblem3N  38311  dih1dimatlem0  38344  djhlsmcl  38430  mapdpglem30  38718  hdmapneg  38862  hgmapval1  38909  hgmapmul  38911  sn-1ne2  39036  zrtelqelz  39070  fltnltalem  39152  3cubeslem3r  39162  3cubeslem4  39164  proot1ex  39679  dirkerper  42258  fourierdlem83  42351  fourierdlem92  42360  sigarperm  42994  sigaradd  43000  fmtnorec1  43576  lincresunit3lem2  44463  itsclc0yqsollem1  44677  itsclinecirc0b  44689  sinhpcosh  44767  amgmwlem  44831
  Copyright terms: Public domain W3C validator