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

Theorem 3eqtr4rd 2867
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 2859 . 2 (𝜑𝐷 = 𝐴)
4 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
53, 4eqtr4d 2859 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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  csbun  4389  csbcnvgALT  5749  csbres  5850  fimacnvinrn2  6834  f1ossf1o  6883  odi  8195  phplem4  8688  cantnfp1lem3  9132  cantnfp1  9133  cardidm  9377  ackbij2lem2  9651  ackbij2lem3  9652  divneg  11321  xadddilem  12677  xadddi2  12680  dfceil2  13199  modlt  13238  modmulnn  13247  seqcaopr3  13395  bcval5  13668  hashgadd  13728  hashun3  13735  hashmap  13786  seqcoll  13812  revccat  14118  cshwmodn  14147  2cshwcom  14168  cshimadifsn0  14182  revco  14186  cshco  14188  ofccat  14319  relexpsucl  14382  cjreb  14472  recj  14473  imcj  14481  imval2  14500  sqrtmul  14609  absmax  14679  amgm2  14719  summolem2a  15062  fsumf1o  15070  sumsnf  15089  sumsplit  15113  fsummulc2  15129  binom  15175  bcxmas  15180  incexclem  15181  incexc  15182  expcnv  15209  pwdif  15213  cvgrat  15229  prodmolem3  15277  prodmolem2a  15278  fprodf1o  15290  prodsn  15306  prodsnf  15308  fprodabs  15318  binomfallfac  15385  fallfacval4  15387  bcfallfac  15388  ege2le3  15433  efaddlem  15436  eftlub  15452  tanval3  15477  tanneg  15491  cosmul  15516  cos01bnd  15529  demoivreALT  15544  flodddiv4  15754  absmulgcd  15887  lcmfunsnlem2  15974  eulerthlem2  16109  phisum  16117  pythagtriplem14  16155  pythagtriplem19  16160  pcmul  16178  pcfac  16225  prmreclem6  16247  4sqlem12  16282  vdwlem6  16312  oppccatid  16979  curf2ndf  17487  oppcyon  17509  joincomALT  17629  meetcomALT  17631  pwsco1mhm  17986  sgrp2nmndlem4  18033  qusgrp2  18157  mulgnngsum  18173  mulgnn0p1  18179  mulgneg  18186  mulgnn0dir  18197  qusghm  18335  gaid  18369  pmtrdifellem3  18537  psgnunilem2  18554  odmulg  18614  sylow1lem2  18655  sylow2a  18675  sylow3lem1  18683  efgredleme  18800  efgcpbllemb  18812  gsumzaddlem  18972  gsumconst  18985  gsumzmhm  18988  ablsimpgfindlem1  19160  srgpcomp  19213  srgbinom  19226  lmodvsmmulgdi  19600  lmodsubdi  19622  rmodislmodlem  19632  0lmhm  19743  lspsneq  19825  qusrhm  19940  quscrng  19943  ascldimulOLD  20047  resspsrmul  20127  evlsscasrng  20240  psropprmul  20336  evls1scasrng  20432  zringlpirlem3  20563  mulgrhm  20575  phssip  20732  frlmip  20852  frlmphl  20855  mat1ghm  21022  mat1mhm  21023  1marepvmarrepid  21114  mdetrlin  21141  mdetrsca2  21143  mdetunilem7  21157  mdetunilem9  21159  mndifsplit  21175  maducoeval2  21179  smadiadetglem2  21211  decpmatmul  21310  pm2mpghm  21354  pm2mpmhmlem2  21357  cpmidgsum2  21417  ptbasfi  22119  ptuni  22132  alexsubALTlem3  22587  subgtgp  22643  tsmsxplem1  22690  xmsusp  23108  restmetu  23109  nminv  23159  nrginvrcnlem  23229  copco  23551  pcoass  23557  pi1bas  23571  pi1xfrf  23586  pi1xfr  23588  isclmp  23630  cph2subdi  23743  cphassr  23745  tcphcphlem1  23767  cphipval  23775  rrxip  23922  rrxnm  23923  pjthlem1  23969  ovolunlem1a  24026  ovolfs2  24101  uniiccdif  24108  ismbf  24158  itgaddlem2  24353  ditgswap  24386  ply1divex  24659  plyeq0lem  24729  plymullem1  24733  dgrcolem1  24792  dgrcolem2  24793  vieta1lem2  24829  elqaalem2  24838  elqaalem3  24839  aaliou3lem7  24867  ulmshft  24907  mulcxplem  25194  cxpmul2  25199  root1eq1  25263  cxpeq  25265  logbchbase  25276  cosangneg2d  25312  isosctrlem2  25324  angpieqvdlem  25333  chordthmlem3  25339  chordthmlem4  25340  chordthmlem5  25341  quad2  25344  dcubic2  25349  cubic2  25353  quart1  25361  scvxcvx  25491  igamlgam  25555  lgam1  25569  basellem9  25594  ppifl  25665  mumul  25686  sgmmul  25705  chtublem  25715  chpub  25724  logfacrlim  25728  dchrsum2  25772  sumdchr2  25774  bposlem9  25796  lgsdir2  25834  lgsdir  25836  lgsdi  25838  lgsdirnn0  25848  lgsdinn0  25849  lgsquad3  25891  2sqblem  25935  chpo1ub  25984  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2if  26001  dchrisum0fmul  26010  rpvmasum2  26016  mulog2sumlem1  26038  vmalogdivsum2  26042  log2sumbnd  26048  selberg3lem1  26061  selberg4lem1  26064  pntrsumo1  26069  selbergr  26072  pntpbnd1  26090  pntlemk  26110  tgbtwnconn1lem3  26288  mideulem2  26448  axlowdimlem16  26671  axcontlem8  26685  vtxval  26713  iedgval  26714  edgval  26762  vtxdgop  27180  finsumvtxdg2size  27260  lp1cycl  27859  ex-ind-dvds  28168  vsfval  28338  lnocoi  28462  nmblolbii  28504  ipasslem5  28540  hvsubid  28731  sshjval3  29059  pjhthlem1  29096  adjval  29595  unopf1o  29621  kbpj  29661  lnopmi  29705  nmcoplbi  29733  cnlnadjlem2  29773  adjadd  29798  branmfn  29810  pjtoi  29884  ofoprabco  30338  hashxpe  30456  splfv3  30560  xrsmulgzz  30593  psgnfzto1stlem  30670  cycpmco2lem5  30700  cycpmco2lem6  30701  cyc3co2  30710  tocyccntz  30714  cyc3genpmlem  30721  cyc3conja  30727  archiabllem1a  30748  gsumvsca1  30782  gsumvsca2  30783  rdivmuldivd  30790  imaslmod  30850  fedgmullem1  30925  submat1n  30970  submatres  30971  madjusmdetlem3  30994  xrge0iifhom  31080  qqhval2lem  31122  qqhrhm  31130  qqhucn  31133  esumsnf  31223  measvunilem0  31372  carsgclctunlem1  31475  ballotlemfp1  31649  ballotlemsf1o  31671  signstfveq0  31747  breprexplemc  31803  breprexp  31804  breprexpnat  31805  circlemeth  31811  logdivsqrle  31821  hgt750lema  31828  revwlk  32269  cvmlift3lem2  32465  cvmlift3lem4  32467  cvmlift3lem5  32468  cvmlift3lem6  32469  cvmlift3lem9  32472  elmrsubrn  32665  bccolsum  32869  bj-bary1lem  34480  csbdif  34489  finixpnum  34759  poimirlem4  34778  poimirlem16  34790  poimirlem19  34793  poimirlem25  34799  mblfinlem3  34813  dvtan  34824  itg2addnc  34828  itgaddnclem2  34833  ftc1anclem6  34854  areacirclem5  34868  areacirc  34869  upixp  34887  prdsbnd2  34956  ismrer1  34999  rngoneglmul  35104  rngoisocnv  35142  islshpsm  35998  lshpnel2N  36003  lfl0f  36087  ldualvsdi1  36161  ldualgrplem  36163  cmtcomlemN  36266  cvlsupr8  36367  pmodl42N  36869  pmapjat1  36871  llnmod2i2  36881  dalawlem2  36890  pmapj2N  36947  idltrn  37168  cdlemc6  37214  cdleme20d  37330  cdleme22e  37362  cdleme22eALTN  37363  cdleme35b  37468  cdleme48fvg  37518  cdlemg4d  37631  cdlemg8a  37645  cdlemg42  37747  cdlemg47a  37752  tendodi1  37802  tendodi2  37803  cdlemk4  37852  cdlemk21N  37891  cdlemk22  37911  cdlemky  37944  cdlemk53b  37974  cdlemk53  37975  cdlemkyyN  37980  erngdvlem3-rN  38016  tendocnv  38039  dia1dim2  38080  dicvaddcl  38208  dihglblem3N  38313  dihmeetlem4preN  38324  dihmeet2  38364  lcfl7lem  38517  baerlem3lem1  38725  baerlem5alem1  38726  mapdh6bN  38755  mapdh6cN  38756  mapdh6dN  38757  hdmap1l6b  38829  hdmap1l6c  38830  hdmap1l6d  38831  hdmap14lem13  38898  nn0expgcd  39064  3cubeslem2  39162  3cubeslem3r  39164  3cubeslem4  39166  pellexlem2  39307  rmxyneg  39397  oddcomabszz  39421  acongeq  39460  hausgraph  39692  fsovrfovd  40235  inductionexd  40385  expgrowth  40547  binomcxplemwb  40560  binomcxplemnn0  40561  binomcxplemnotnn0  40568  sumsnd  41163  restuni4  41268  fmuldfeqlem1  41743  cncfmptss  41748  climexp  41766  dvresntr  42082  stoweidlem17  42183  wallispi  42236  dirkertrigeq  42267  dirkercncflem2  42270  fourierdlem30  42303  fourierdlem41  42314  fourierdlem81  42353  fourierdlem103  42375  sge0xp  42592  sge0isummpt2  42595  isomennd  42694  vonioolem1  42843  sigarperm  42998  prprspr2  43527  opoeALTV  43695  c0mgm  44078  c0mhm  44079  zrrnghm  44086  cznrng  44124  rngchomrnghmresALTV  44165  fdmdifeqresdif  44288  lincsum  44382  lincscm  44383  lmod1lem4  44443  blennngt2o2  44550  blennn0e2  44552  reccot  44755  rectan  44756  cotsqcscsq  44759  amgmlemALT  44802
  Copyright terms: Public domain W3C validator