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

Theorem 3eqtr4rd 2654
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1 (𝜑𝐴 = 𝐵)
3eqtr4d.2 (𝜑𝐶 = 𝐴)
3eqtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3eqtr4rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
2 3eqtr4d.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2eqtr4d 2646 . 2 (𝜑𝐷 = 𝐴)
4 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
53, 4eqtr4d 2646 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  csbun  3960  csbcnvgALT  5217  csbres  5307  fimacnvinrn2  6242  odi  7523  phplem4  8004  cantnfp1lem3  8437  cantnfp1  8438  cardidm  8645  ackbij2lem2  8922  ackbij2lem3  8923  divneg  10568  xadddilem  11953  xadddi2  11956  dfceil2  12457  modlt  12496  modmulnn  12505  seqcaopr3  12653  bcval5  12922  hashgadd  12979  hashun3  12986  seqcoll  13057  swrdccatwrd  13266  cshwmodn  13338  2cshwcom  13359  cshimadifsn0  13373  revco  13377  cshco  13379  ofccat  13502  relexpsucl  13567  cjreb  13657  recj  13658  imcj  13666  imval2  13685  sqrtmul  13794  absmax  13863  amgm2  13903  summolem2a  14239  fsumf1o  14247  sumsn  14265  sumsplit  14287  fsummulc2  14304  binom  14347  bcxmas  14352  incexclem  14353  incexc  14354  expcnv  14381  cvgrat  14400  prodmolem3  14448  prodmolem2a  14449  fprodf1o  14461  prodsn  14477  prodsnf  14479  fprodabs  14489  binomfallfac  14557  fallfacval4  14559  bcfallfac  14560  ege2le3  14605  efaddlem  14608  eftlub  14624  tanval3  14649  tanneg  14663  cosmul  14688  cos01bnd  14701  demoivreALT  14716  flodddiv4  14921  absmulgcd  15050  lcmfunsnlem2  15137  eulerthlem2  15271  phisum  15279  pythagtriplem14  15317  pcmul  15340  pcfac  15387  prmreclem6  15409  4sqlem12  15444  vdwlem6  15474  oppccatid  16148  curf2ndf  16656  oppcyon  16678  joincomALT  16798  meetcomALT  16800  pwsco1mhm  17139  sgrp2nmndlem4  17184  qusgrp2  17302  mulgnn0p1  17321  mulgneg  17329  mulgnn0dir  17340  qusghm  17466  gaid  17501  pmtrdifellem3  17667  psgnunilem2  17684  odmulg  17742  sylow1lem2  17783  sylow2a  17803  sylow3lem1  17811  efgredleme  17925  efgcpbllemb  17937  gsumzaddlem  18090  gsumconst  18103  gsumzmhm  18106  srgpcomp  18301  srgbinom  18314  lmodvsmmulgdi  18667  lmodsubdi  18689  0lmhm  18807  lspsneq  18889  qusrhm  19004  quscrng  19007  asclrhm  19109  resspsrmul  19184  evlsscasrng  19293  psropprmul  19375  evls1scasrng  19470  zringlpirlem3  19599  mulgrhm  19610  frlmip  19878  frlmphl  19881  mat1ghm  20050  mat1mhm  20051  1marepvmarrepid  20142  mdetrlin  20169  mdetrsca2  20171  mdetunilem7  20185  mdetunilem9  20187  mndifsplit  20203  maducoeval2  20207  smadiadetglem2  20239  decpmatmul  20338  pm2mpghm  20382  pm2mpmhmlem2  20385  cpmidgsum2  20445  ptbasfi  21136  ptuni  21149  alexsubALTlem3  21605  subgtgp  21661  tsmsxplem1  21708  xmsusp  22125  restmetu  22126  nminv  22175  nrginvrcnlem  22238  copco  22557  pcoass  22563  pi1bas  22577  pi1xfrf  22592  pi1xfr  22594  isclmp  22636  cph2subdi  22741  cphassr  22743  tchcphlem1  22763  rrxip  22903  rrxnm  22904  pjthlem1  22933  ovolunlem1a  22988  ovolfs2  23062  uniiccdif  23069  ismbf  23120  itgaddlem2  23313  ditgswap  23346  ply1divex  23617  plyeq0lem  23687  plymullem1  23691  dgrcolem2  23751  vieta1lem2  23787  elqaalem2  23796  elqaalem3  23797  aaliou3lem7  23825  ulmshft  23865  mulcxplem  24147  cxpmul2  24152  root1eq1  24213  cxpeq  24215  logbchbase  24226  cosangneg2d  24254  isosctrlem2  24266  angpieqvdlem  24272  chordthmlem3  24278  chordthmlem4  24279  chordthmlem5  24280  quad2  24283  dcubic2  24288  cubic2  24292  quart1  24300  scvxcvx  24429  igamlgam  24493  lgam1  24507  basellem9  24532  ppifl  24603  mumul  24624  sgmmul  24643  chtublem  24653  chpub  24662  logfacrlim  24666  dchrsum2  24710  sumdchr2  24712  bposlem9  24734  lgsdir2  24772  lgsdir  24774  lgsdi  24776  lgsdirnn0  24786  lgsdinn0  24787  lgsquad3  24829  2sqblem  24873  chpo1ub  24886  dchrmusum2  24900  dchrvmasumlem1  24901  dchrvmasum2if  24903  dchrisum0fmul  24912  rpvmasum2  24918  mulog2sumlem1  24940  vmalogdivsum2  24944  log2sumbnd  24950  selberg3lem1  24963  selberg4lem1  24966  pntrsumo1  24971  selbergr  24974  pntpbnd1  24992  pntlemk  25012  tgbtwnconn1lem3  25187  mideulem2  25344  axlowdimlem16  25555  axcontlem8  25569  clwlkfoclwwlk  26138  ex-ind-dvds  26476  vsfval  26658  lnocoi  26802  nmblolbii  26844  ipasslem5  26880  hvsubid  27073  sshjval3  27403  pjhthlem1  27440  adjval  27939  unopf1o  27965  kbpj  28005  lnopmi  28049  nmcoplbi  28077  cnlnadjlem2  28117  adjadd  28142  branmfn  28154  pjtoi  28228  ofoprabco  28653  xrsmulgzz  28815  archiabllem1a  28882  gsumvsca1  28919  gsumvsca2  28920  rdivmuldivd  28928  psgnfzto1stlem  28987  submat1n  29005  submatres  29006  madjusmdetlem3  29029  xrge0iifhom  29117  qqhval2lem  29159  qqhrhm  29167  qqhucn  29170  esumsnf  29259  measvunilem0  29409  carsgclctunlem1  29512  ballotlemfp1  29686  ballotlemsf1o  29708  signstfveq0  29786  cvmlift3lem2  30362  cvmlift3lem4  30364  cvmlift3lem5  30365  cvmlift3lem6  30366  cvmlift3lem9  30369  elmrsubrn  30477  bccolsum  30684  bj-bary1lem  32133  csbdif  32143  finixpnum  32360  poimirlem4  32379  poimirlem16  32391  poimirlem19  32394  poimirlem25  32400  mblfinlem3  32414  dvtan  32426  itg2addnc  32430  itgaddnclem2  32435  ftc1anclem6  32456  areacirclem5  32470  areacirc  32471  upixp  32490  prdsbnd2  32560  ismrer1  32603  rngoneglmul  32708  rngoisocnv  32746  islshpsm  33081  lshpnel2N  33086  lfl0f  33170  ldualvsdi1  33244  ldualgrplem  33246  cmtcomlemN  33349  cvlsupr8  33450  pmodl42N  33951  pmapjat1  33953  llnmod2i2  33963  dalawlem2  33972  pmapj2N  34029  idltrn  34250  cdlemc6  34297  cdleme20d  34414  cdleme22e  34446  cdleme22eALTN  34447  cdleme35b  34552  cdleme48fvg  34602  cdlemg4d  34715  cdlemg8a  34729  cdlemg42  34831  cdlemg47a  34836  tendodi1  34886  tendodi2  34887  cdlemk4  34936  cdlemk21N  34975  cdlemk22  34995  cdlemky  35028  cdlemk53b  35058  cdlemk53  35059  cdlemkyyN  35064  erngdvlem3-rN  35100  tendocnv  35124  dia1dim2  35165  dicvaddcl  35293  dihglblem3N  35398  dihmeetlem4preN  35409  dihmeet2  35449  lcfl7lem  35602  baerlem3lem1  35810  baerlem5alem1  35811  mapdh6bN  35840  mapdh6cN  35841  mapdh6dN  35842  hdmap1l6b  35915  hdmap1l6c  35916  hdmap1l6d  35917  hdmap14lem13  35986  pellexlem2  36208  rmxyneg  36299  oddcomabszz  36323  acongeq  36364  hausgraph  36605  fsovrfovd  37119  inductionexd  37269  expgrowth  37352  binomcxplemwb  37365  binomcxplemnn0  37366  binomcxplemnotnn0  37373  sumsnd  38004  restuni4  38132  sumsnf  38433  fmuldfeqlem1  38446  cncfmptss  38451  climexp  38469  dvresntr  38603  stoweidlem17  38707  wallispi  38760  dirkertrigeq  38791  dirkercncflem2  38794  fourierdlem30  38827  fourierdlem41  38838  fourierdlem81  38877  fourierdlem103  38899  sge0xp  39119  sge0isummpt2  39122  isomennd  39218  vonioolem1  39368  sigarperm  39495  pwdif  39837  opoeALTV  39930  clwlksfoclwwlk  41265  lp1cycl  41314  c0mgm  41694  c0mhm  41695  zrrnghm  41702  cznrng  41742  rngchomrnghmresALTV  41783  fdmdifeqresdif  41908  lincsum  42007  lincscm  42008  lmod1lem4  42068  blennngt2o2  42179  blennn0e2  42181  reccot  42254  rectan  42255  cotsqcscsq  42258  amgmlemALT  42314
  Copyright terms: Public domain W3C validator