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

Theorem 3eqtr4rd 2474
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
2 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2eqtr4d 2466 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2466 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414
This theorem is referenced by:  csbun  3826  csbcnvgALT  5035  csbres  5124  odi  7285  phplem4  7757  cantnfp1lem3  8187  cantnfp1  8188  cardidm  8395  ackbij2lem2  8671  ackbij2lem3  8672  divneg  10303  xadddilem  11581  xadddi2  11584  dfceil2  12068  modlt  12107  modmulnn  12114  seqcaopr3  12248  bcval5  12503  hashgadd  12556  hashun3  12563  seqcoll  12625  swrdccatwrd  12815  cshwmodn  12888  2cshwcom  12906  revco  12922  cshco  12924  relexpsucl  13085  cjreb  13175  recj  13176  imcj  13184  imval2  13203  sqrtmul  13312  absmax  13381  amgm2  13421  summolem2a  13769  fsumf1o  13777  sumsn  13795  sumsplit  13817  fsummulc2  13833  binom  13876  bcxmas  13881  incexclem  13882  incexc  13883  expcnv  13910  cvgrat  13927  prodmolem3  13975  prodmolem2a  13976  fprodf1o  13988  prodsn  14004  prodsnf  14006  fprodabs  14016  binomfallfac  14082  fallfacval4  14084  bcfallfac  14085  ege2le3  14132  efaddlem  14135  eftlub  14151  tanval3  14176  tanneg  14190  cosmul  14215  cos01bnd  14228  demoivreALT  14243  absmulgcd  14503  lcmfunsnlem2  14601  eulerthlem2  14718  pythagtriplem14  14766  pcmul  14789  pcfac  14832  prmreclem6  14853  4sqlem12  14888  vdwlem6  14924  oppccatid  15612  curf2ndf  16120  oppcyon  16142  joincomALT  16263  meetcomALT  16265  pwsco1mhm  16605  sgrp2nmndlem4  16650  mulgnn0p1  16757  mulgneg  16764  mulgnn0dir  16769  qusgrp2  16792  qusghm  16907  gaid  16941  pmtrdifellem3  17107  psgnunilem2  17124  odmulg  17195  sylow1lem2  17239  sylow2a  17259  sylow3lem1  17267  efgredleme  17381  efgcpbllemb  17393  gsumzaddlem  17542  gsumconst  17555  gsumzmhm  17558  srgpcomp  17753  srgbinom  17766  lmodvsmmulgdi  18114  lmodsubdi  18133  0lmhm  18251  lspsneq  18333  qusrhm  18449  quscrng  18452  asclrhm  18554  resspsrmul  18629  evlsscasrng  18737  psropprmul  18819  evls1scasrng  18915  zringlpirlem3OLD  19042  zringlpirlem3  19044  mulgrhm  19056  frlmip  19323  frlmphl  19326  mat1ghm  19495  mat1mhm  19496  1marepvmarrepid  19587  mdetrlin  19614  mdetrsca2  19616  mdetunilem7  19630  mdetunilem9  19632  mndifsplit  19648  maducoeval2  19652  smadiadetglem2  19684  decpmatmul  19783  pm2mpghm  19827  pm2mpmhmlem2  19830  cpmidgsum2  19890  ptbasfi  20583  ptuni  20596  alexsubALTlem3  21051  subgtgp  21107  tsmsxplem1  21154  xmsusp  21571  restmetu  21572  nminv  21621  nrginvrcnlem  21680  copco  22036  pcoass  22042  pi1bas  22056  pi1xfrf  22071  pi1xfr  22073  cph2subdi  22174  cphassr  22176  tchcphlem1  22196  rrxip  22336  rrxnm  22337  pjthlem1  22378  ovolunlem1a  22436  ovolfs2  22510  uniiccdif  22522  ismbf  22573  itgaddlem2  22768  ditgswap  22801  ply1divex  23074  plyeq0lem  23151  plymullem1  23155  dgrcolem2  23215  vieta1lem2  23251  elqaalem2  23260  elqaalem3  23261  elqaalem2OLD  23263  elqaalem3OLD  23264  aaliou3lem7  23292  ulmshft  23332  mulcxplem  23616  cxpmul2  23621  root1eq1  23682  cxpeq  23684  logbchbase  23695  cosangneg2d  23723  isosctrlem2  23735  angpieqvdlem  23741  chordthmlem3  23747  chordthmlem4  23748  chordthmlem5  23749  quad2  23752  dcubic2  23757  cubic2  23761  quart1  23769  scvxcvx  23898  igamlgam  23962  lgam1  23976  basellem9  24002  ppifl  24074  mumul  24095  sgmmul  24116  chtublem  24126  chpub  24135  logfacrlim  24139  dchrsum2  24183  sumdchr2  24185  bposlem9  24207  lgsdir2  24243  lgsdir  24245  lgsdi  24247  lgsdirnn0  24254  lgsdinn0  24255  lgsquad3  24276  2sqblem  24292  chpo1ub  24305  dchrmusum2  24319  dchrvmasumlem1  24320  dchrvmasum2if  24322  dchrisum0fmul  24331  rpvmasum2  24337  mulog2sumlem1  24359  vmalogdivsum2  24363  log2sumbnd  24369  selberg3lem1  24382  selberg4lem1  24385  pntrsumo1  24390  selbergr  24393  pntpbnd1  24411  pntlemk  24431  tgbtwnconn1lem3  24606  mideulem2  24763  axlowdimlem16  24974  axcontlem8  24988  clwlkfoclwwlk  25559  ex-ind-dvds  25885  gxnn0suc  25978  gxinv  25984  vsfval  26240  lnocoi  26384  nmblolbii  26426  ipasslem5  26462  hvsubid  26665  sshjval3  26993  pjhthlem1  27030  adjval  27529  unopf1o  27555  kbpj  27595  lnopmi  27639  nmcoplbi  27667  cnlnadjlem2  27707  adjadd  27732  branmfn  27744  pjtoi  27818  fimacnvinrn2  28226  ofoprabco  28257  xrsmulgzz  28435  archiabllem1a  28503  gsumvsca1  28541  gsumvsca2  28542  rdivmuldivd  28550  psgnfzto1stlem  28609  submat1n  28627  submatres  28628  madjusmdetlem3  28651  xrge0iifhom  28739  qqhval2lem  28781  qqhrhm  28789  qqhucn  28792  esumsnf  28881  measvunilem0  29031  carsgclctunlem1  29145  ballotlemsf1o  29342  ballotlemsf1oOLD  29380  ofccat  29425  signstfveq0  29462  cvmlift3lem2  30039  cvmlift3lem4  30041  cvmlift3lem5  30042  cvmlift3lem6  30043  cvmlift3lem9  30046  elmrsubrn  30154  bccolsum  30370  bj-bary1lem  31667  csbdif  31677  finixpnum  31844  poimirlem4  31858  poimirlem16  31870  poimirlem19  31873  poimirlem25  31879  mblfinlem3  31893  dvtan  31906  itg2addnc  31910  itgaddnclem2  31915  ftc1anclem6  31936  areacirclem5  31950  areacirc  31951  upixp  31970  prdsbnd2  32041  ismrer1  32084  rngoneglmul  32104  rngoisocnv  32134  islshpsm  32465  lshpnel2N  32470  lfl0f  32554  ldualvsdi1  32628  ldualgrplem  32630  cmtcomlemN  32733  cvlsupr8  32834  pmodl42N  33335  pmapjat1  33337  llnmod2i2  33347  dalawlem2  33356  pmapj2N  33413  idltrn  33634  cdlemc6  33681  cdleme20d  33798  cdleme22e  33830  cdleme22eALTN  33831  cdleme35b  33936  cdleme48fvg  33986  cdlemg4d  34099  cdlemg8a  34113  cdlemg42  34215  cdlemg47a  34220  tendodi1  34270  tendodi2  34271  cdlemk4  34320  cdlemk21N  34359  cdlemk22  34379  cdlemky  34412  cdlemk53b  34442  cdlemk53  34443  cdlemkyyN  34448  erngdvlem3-rN  34484  tendocnv  34508  dia1dim2  34549  dicvaddcl  34677  dihglblem3N  34782  dihmeetlem4preN  34793  dihmeet2  34833  lcfl7lem  34986  baerlem3lem1  35194  baerlem5alem1  35195  mapdh6bN  35224  mapdh6cN  35225  mapdh6dN  35226  hdmap1l6b  35299  hdmap1l6c  35300  hdmap1l6d  35301  hdmap14lem13  35370  pellexlem2  35594  rmxyneg  35688  oddcomabszz  35712  acongeq  35753  phisum  35996  hausgraph  36009  inductionexd  36451  expgrowth  36542  binomcxplemwb  36555  binomcxplemnn0  36556  binomcxplemnotnn0  36563  sumsnd  37208  sumsnf  37471  fmuldfeqlem1  37480  cncfmptss  37485  climexp  37503  dvresntr  37608  stoweidlem17  37697  wallispi  37752  dirkertrigeq  37783  dirkercncflem2  37786  fourierdlem30  37819  fourierdlem41  37831  fourierdlem81  37871  fourierdlem103  37893  sge0xp  38059  sge0isummpt2  38062  isomennd  38131  sigarperm  38182  opoeALTV  38524  c0mgm  39181  c0mhm  39182  zrrnghm  39189  cznrng  39229  rngchomrnghmresALTV  39270  fdmdifeqresdif  39397  lincsum  39496  lincscm  39497  lmod1lem4  39557  blennngt2o2  39677  blennn0e2  39679  reccot  39752  rectan  39753  cotsqcscsq  39756
  Copyright terms: Public domain W3C validator