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

Theorem 3eqtr4rd 2476
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 2468 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2468 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  csbun  3697  csbcnvgOLD  5011  csbres  5100  odi  7006  phplem4  7481  cantnfp1lem3  7876  cantnfp1  7877  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cardidm  8117  ackbij2lem2  8397  ackbij2lem3  8398  divneg  10014  xadddilem  11245  xadddi2  11248  dfceil2  11664  modlt  11702  modmulnn  11709  seqcaopr3  11825  bcval5  12078  hashgadd  12124  hashun3  12131  seqcoll  12200  swrdccatwrd  12346  cshwmodn  12416  2cshwcom  12434  revco  12446  cshco  12448  cjreb  12596  recj  12597  imcj  12605  imval2  12624  sqrmul  12733  absmax  12801  amgm2  12841  summolem2a  13176  fsumf1o  13184  sumsn  13201  sumsplit  13219  fsummulc2  13234  binom  13276  bcxmas  13281  incexclem  13282  incexc  13283  expcnv  13309  cvgrat  13326  ege2le3  13358  efaddlem  13361  eftlub  13376  tanval3  13401  tanneg  13415  cosmul  13440  cos01bnd  13453  demoivreALT  13468  absmulgcd  13714  eulerthlem2  13840  pythagtriplem14  13878  pcmul  13901  pcfac  13944  prmreclem6  13965  4sqlem12  14000  vdwlem6  14030  oppccatid  14641  curf2ndf  15040  oppcyon  15062  joincomALT  15182  meetcomALT  15184  pwsco1mhm  15480  mulgnn0p1  15618  mulgneg  15625  mulgnn0dir  15630  divsgrp2  15653  divsghm  15763  gaid  15797  pmtrdifellem3  15964  psgnunilem2  15981  odmulg  16037  sylow1lem2  16078  sylow2a  16098  sylow3lem1  16106  efgredleme  16220  efgcpbllemb  16232  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  lmodsubdi  16926  0lmhm  17043  lspsneq  17125  divsrhm  17241  divscrng  17244  asclrhm  17334  resspsrmul  17423  psropprmul  17591  zringlpirlem3  17747  zlpirlem3  17752  mulgrhm  17768  mulgrhmOLD  17771  frlmip  18045  frlmphl  18048  1marepvmarrepid  18228  mdet1  18250  mdetrlin  18251  mdetrsca2  18253  mdetunilem7  18266  mdetunilem9  18268  mndifsplit  18284  maducoeval2  18288  smadiadetglem2  18320  ptbasfi  18996  ptuni  19009  alexsubALTlem3  19463  subgtgp  19518  tsmsxplem1  19569  xmsuspOLD  20002  xmsusp  20003  restmetu  20004  nminv  20054  nrginvrcnlem  20113  copco  20432  pcoass  20438  pi1bas  20452  pi1xfrf  20467  pi1xfr  20469  cph2subdi  20570  cphassr  20572  tchcphlem1  20592  rrxip  20736  rrxnm  20737  pjthlem1  20766  ovolunlem1a  20821  ovolfs2  20893  uniiccdif  20900  ismbf  20950  itgaddlem2  21143  ditgswap  21176  ply1divex  21493  plyeq0lem  21563  plymullem1  21567  dgrcolem2  21626  vieta1lem2  21662  elqaalem2  21671  elqaalem3  21672  aaliou3lem7  21700  ulmshft  21740  mulcxplem  22014  cxpmul2  22019  root1eq1  22078  cxpeq  22080  cosangneg2d  22088  isosctrlem2  22102  angpieqvdlem  22108  chordthmlem3  22114  chordthmlem4  22115  chordthmlem5  22116  quad2  22119  dcubic2  22124  cubic2  22128  quart1  22136  scvxcvx  22264  basellem9  22311  ppifl  22383  mumul  22404  sgmmul  22425  chtublem  22435  chpub  22444  logfacrlim  22448  dchrsum2  22492  sumdchr2  22494  bposlem9  22516  lgsdir2  22552  lgsdir  22554  lgsdi  22556  lgsdirnn0  22563  lgsdinn0  22564  2sqblem  22601  chpo1ub  22614  dchrmusum2  22628  dchrvmasumlem1  22629  dchrvmasum2if  22631  dchrisum0fmul  22640  rpvmasum2  22646  mulog2sumlem1  22668  vmalogdivsum2  22672  log2sumbnd  22678  selberg3lem1  22691  selberg4lem1  22694  pntrsumo1  22699  selbergr  22702  pntpbnd1  22720  pntlemk  22740  axlowdimlem16  23026  axcontlem8  23040  gxnn0suc  23574  gxinv  23580  vsfval  23836  lnocoi  23980  nmblolbii  24022  ipasslem5  24058  hvsubid  24251  sshjval3  24580  pjhthlem1  24617  adjval  25117  unopf1o  25143  kbpj  25183  lnopmi  25227  nmcoplbi  25255  cnlnadjlem2  25295  adjadd  25320  branmfn  25332  pjtoi  25406  fimacnvinrn2  25777  ofoprabco  25806  xrsmulgzz  25962  xrge0adddir  25979  archiabllem1a  26032  gsumvsca1  26104  gsumvsca2  26105  rdivmuldivd  26112  xrge0iifhom  26221  qqhval2lem  26264  qqhrhm  26272  esumsn  26369  measvunilem0  26481  ballotlemsf1o  26744  ofccat  26789  signstfveq0  26826  igamlgam  26884  lgam1  26898  cvmlift3lem2  27057  cvmlift3lem4  27059  cvmlift3lem5  27060  cvmlift3lem6  27061  cvmlift3lem9  27064  prodmolem3  27293  prodmolem2a  27294  fprodf1o  27306  prodsn  27320  fprodabs  27331  binomfallfac  27391  fallfacval4  27393  bcfallfac  27394  finixpnum  28258  mblfinlem3  28274  dvtan  28286  itg2addnc  28290  itgaddnclem2  28295  ftc1anclem6  28316  areacirclem5  28332  areacirc  28333  upixp  28467  prdsbnd2  28538  ismrer1  28581  rngoneglmul  28601  rngoisocnv  28631  pellexlem2  29016  rmxyneg  29106  oddcomabszz  29130  acongeq  29171  phisum  29412  hausgraph  29425  expgrowth  29454  sumsnd  29593  fmuldfeqlem1  29608  cncfmptss  29613  climexp  29624  stoweidlem17  29658  wallispi  29711  sigarperm  29742  clwlkfoclwwlk  30364  fdmdifeqresdif  30576  lincsum  30672  lincscm  30673  reccot  30802  rectan  30803  cotsqcscsq  30806  bj-bary1lem  32174  islshpsm  32198  lshpnel2N  32203  lfl0f  32287  ldualvsdi1  32361  ldualgrplem  32363  cmtcomlemN  32466  cvlsupr8  32567  pmodl42N  33068  pmapjat1  33070  llnmod2i2  33080  dalawlem2  33089  pmapj2N  33146  idltrn  33367  cdlemc6  33413  cdleme20d  33529  cdleme22e  33561  cdleme22eALTN  33562  cdleme35b  33667  cdleme48fvg  33717  cdlemg4d  33830  cdlemg8a  33844  cdlemg42  33946  cdlemg47a  33951  tendodi1  34001  tendodi2  34002  cdlemk4  34051  cdlemk21N  34090  cdlemk22  34110  cdlemky  34143  cdlemk53b  34173  cdlemk53  34174  cdlemkyyN  34179  erngdvlem3-rN  34215  tendocnv  34239  dia1dim2  34280  dicvaddcl  34408  dihglblem3N  34513  dihmeetlem4preN  34524  dihmeet2  34564  lcfl7lem  34717  baerlem3lem1  34925  baerlem5alem1  34926  mapdh6bN  34955  mapdh6cN  34956  mapdh6dN  34957  hdmap1l6b  35030  hdmap1l6c  35031  hdmap1l6d  35032  hdmap14lem13  35101
  Copyright terms: Public domain W3C validator