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

Theorem 3eqtr4rd 2481
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 2473 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2473 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  csbun  3704  csbcnvgALT  5019  csbres  5108  odi  7010  phplem4  7485  cantnfp1lem3  7880  cantnfp1  7881  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cardidm  8121  ackbij2lem2  8401  ackbij2lem3  8402  divneg  10018  xadddilem  11249  xadddi2  11252  dfceil2  11672  modlt  11710  modmulnn  11717  seqcaopr3  11833  bcval5  12086  hashgadd  12132  hashun3  12139  seqcoll  12208  swrdccatwrd  12354  cshwmodn  12424  2cshwcom  12442  revco  12454  cshco  12456  cjreb  12604  recj  12605  imcj  12613  imval2  12632  sqrmul  12741  absmax  12809  amgm2  12849  summolem2a  13184  fsumf1o  13192  sumsn  13209  sumsplit  13227  fsummulc2  13243  binom  13285  bcxmas  13290  incexclem  13291  incexc  13292  expcnv  13318  cvgrat  13335  ege2le3  13367  efaddlem  13370  eftlub  13385  tanval3  13410  tanneg  13424  cosmul  13449  cos01bnd  13462  demoivreALT  13477  absmulgcd  13723  eulerthlem2  13849  pythagtriplem14  13887  pcmul  13910  pcfac  13953  prmreclem6  13974  4sqlem12  14009  vdwlem6  14039  oppccatid  14650  curf2ndf  15049  oppcyon  15071  joincomALT  15191  meetcomALT  15193  pwsco1mhm  15489  mulgnn0p1  15629  mulgneg  15636  mulgnn0dir  15641  divsgrp2  15664  divsghm  15774  gaid  15808  pmtrdifellem3  15975  psgnunilem2  15992  odmulg  16048  sylow1lem2  16089  sylow2a  16109  sylow3lem1  16117  efgredleme  16231  efgcpbllemb  16243  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  srgpcomp  16619  srgbinom  16631  lmodsubdi  16980  0lmhm  17098  lspsneq  17180  divsrhm  17296  divscrng  17299  asclrhm  17389  resspsrmul  17466  evlsscasrng  17587  psropprmul  17668  evls1scasrng  17748  zringlpirlem3  17880  zlpirlem3  17885  mulgrhm  17901  mulgrhmOLD  17904  frlmip  18178  frlmphl  18181  1marepvmarrepid  18361  mdet1  18383  mdetrlin  18384  mdetrsca2  18386  mdetunilem7  18399  mdetunilem9  18401  mndifsplit  18417  maducoeval2  18421  smadiadetglem2  18453  ptbasfi  19129  ptuni  19142  alexsubALTlem3  19596  subgtgp  19651  tsmsxplem1  19702  xmsuspOLD  20135  xmsusp  20136  restmetu  20137  nminv  20187  nrginvrcnlem  20246  copco  20565  pcoass  20571  pi1bas  20585  pi1xfrf  20600  pi1xfr  20602  cph2subdi  20703  cphassr  20705  tchcphlem1  20725  rrxip  20869  rrxnm  20870  pjthlem1  20899  ovolunlem1a  20954  ovolfs2  21026  uniiccdif  21033  ismbf  21083  itgaddlem2  21276  ditgswap  21309  ply1divex  21583  plyeq0lem  21653  plymullem1  21657  dgrcolem2  21716  vieta1lem2  21752  elqaalem2  21761  elqaalem3  21762  aaliou3lem7  21790  ulmshft  21830  mulcxplem  22104  cxpmul2  22109  root1eq1  22168  cxpeq  22170  cosangneg2d  22178  isosctrlem2  22192  angpieqvdlem  22198  chordthmlem3  22204  chordthmlem4  22205  chordthmlem5  22206  quad2  22209  dcubic2  22214  cubic2  22218  quart1  22226  scvxcvx  22354  basellem9  22401  ppifl  22473  mumul  22494  sgmmul  22515  chtublem  22525  chpub  22534  logfacrlim  22538  dchrsum2  22582  sumdchr2  22584  bposlem9  22606  lgsdir2  22642  lgsdir  22644  lgsdi  22646  lgsdirnn0  22653  lgsdinn0  22654  2sqblem  22691  chpo1ub  22704  dchrmusum2  22718  dchrvmasumlem1  22719  dchrvmasum2if  22721  dchrisum0fmul  22730  rpvmasum2  22736  mulog2sumlem1  22758  vmalogdivsum2  22762  log2sumbnd  22768  selberg3lem1  22781  selberg4lem1  22784  pntrsumo1  22789  selbergr  22792  pntpbnd1  22810  pntlemk  22830  axlowdimlem16  23154  axcontlem8  23168  gxnn0suc  23702  gxinv  23708  vsfval  23964  lnocoi  24108  nmblolbii  24150  ipasslem5  24186  hvsubid  24379  sshjval3  24708  pjhthlem1  24745  adjval  25245  unopf1o  25271  kbpj  25311  lnopmi  25355  nmcoplbi  25383  cnlnadjlem2  25423  adjadd  25448  branmfn  25460  pjtoi  25534  fimacnvinrn2  25904  ofoprabco  25933  xrsmulgzz  26090  xrge0adddir  26106  archiabllem1a  26159  gsumvsca1  26202  gsumvsca2  26203  rdivmuldivd  26210  xrge0iifhom  26319  qqhval2lem  26362  qqhrhm  26370  esumsn  26467  measvunilem0  26579  ballotlemsf1o  26848  ofccat  26893  signstfveq0  26930  igamlgam  26988  lgam1  27002  cvmlift3lem2  27161  cvmlift3lem4  27163  cvmlift3lem5  27164  cvmlift3lem6  27165  cvmlift3lem9  27168  prodmolem3  27397  prodmolem2a  27398  fprodf1o  27410  prodsn  27424  fprodabs  27435  binomfallfac  27495  fallfacval4  27497  bcfallfac  27498  finixpnum  28367  mblfinlem3  28383  dvtan  28395  itg2addnc  28399  itgaddnclem2  28404  ftc1anclem6  28425  areacirclem5  28441  areacirc  28442  upixp  28576  prdsbnd2  28647  ismrer1  28690  rngoneglmul  28710  rngoisocnv  28740  pellexlem2  29124  rmxyneg  29214  oddcomabszz  29238  acongeq  29279  phisum  29520  hausgraph  29533  expgrowth  29562  sumsnd  29701  fmuldfeqlem1  29716  cncfmptss  29721  climexp  29731  stoweidlem17  29765  wallispi  29818  sigarperm  29849  clwlkfoclwwlk  30471  fdmdifeqresdif  30684  lmodvsmmulgdi  30752  lincsum  30852  lincscm  30853  reccot  30982  rectan  30983  cotsqcscsq  30986  bj-bary1lem  32441  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  33680  cdleme20d  33796  cdleme22e  33828  cdleme22eALTN  33829  cdleme35b  33934  cdleme48fvg  33984  cdlemg4d  34097  cdlemg8a  34111  cdlemg42  34213  cdlemg47a  34218  tendodi1  34268  tendodi2  34269  cdlemk4  34318  cdlemk21N  34357  cdlemk22  34377  cdlemky  34410  cdlemk53b  34440  cdlemk53  34441  cdlemkyyN  34446  erngdvlem3-rN  34482  tendocnv  34506  dia1dim2  34547  dicvaddcl  34675  dihglblem3N  34780  dihmeetlem4preN  34791  dihmeet2  34831  lcfl7lem  34984  baerlem3lem1  35192  baerlem5alem1  35193  mapdh6bN  35222  mapdh6cN  35223  mapdh6dN  35224  hdmap1l6b  35297  hdmap1l6c  35298  hdmap1l6d  35299  hdmap14lem13  35368
  Copyright terms: Public domain W3C validator