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

Theorem 3eqtr4rd 2696
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 2688 . 2 (𝜑𝐷 = 𝐴)
4 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
53, 4eqtr4d 2688 1 (𝜑𝐷 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  csbun  4042  csbcnvgALT  5339  csbres  5431  fimacnvinrn2  6389  odi  7704  phplem4  8183  cantnfp1lem3  8615  cantnfp1  8616  cardidm  8823  ackbij2lem2  9100  ackbij2lem3  9101  divneg  10757  xadddilem  12162  xadddi2  12165  dfceil2  12680  modlt  12719  modmulnn  12728  seqcaopr3  12876  bcval5  13145  hashgadd  13204  hashun3  13211  seqcoll  13286  swrdccatwrd  13514  cshwmodn  13587  2cshwcom  13608  cshimadifsn0  13622  revco  13626  cshco  13628  ofccat  13754  relexpsucl  13817  cjreb  13907  recj  13908  imcj  13916  imval2  13935  sqrtmul  14044  absmax  14113  amgm2  14153  summolem2a  14490  fsumf1o  14498  sumsnf  14517  sumsn  14519  sumsplit  14543  fsummulc2  14560  binom  14606  bcxmas  14611  incexclem  14612  incexc  14613  expcnv  14640  cvgrat  14659  prodmolem3  14707  prodmolem2a  14708  fprodf1o  14720  prodsn  14736  prodsnf  14738  fprodabs  14748  binomfallfac  14816  fallfacval4  14818  bcfallfac  14819  ege2le3  14864  efaddlem  14867  eftlub  14883  tanval3  14908  tanneg  14922  cosmul  14947  cos01bnd  14960  demoivreALT  14975  flodddiv4  15184  absmulgcd  15313  lcmfunsnlem2  15400  eulerthlem2  15534  phisum  15542  pythagtriplem14  15580  pcmul  15603  pcfac  15650  prmreclem6  15672  4sqlem12  15707  vdwlem6  15737  oppccatid  16426  curf2ndf  16934  oppcyon  16956  joincomALT  17076  meetcomALT  17078  pwsco1mhm  17417  sgrp2nmndlem4  17462  qusgrp2  17580  mulgnn0p1  17599  mulgneg  17607  mulgnn0dir  17618  qusghm  17744  gaid  17778  pmtrdifellem3  17944  psgnunilem2  17961  odmulg  18019  sylow1lem2  18060  sylow2a  18080  sylow3lem1  18088  efgredleme  18202  efgcpbllemb  18214  gsumzaddlem  18367  gsumconst  18380  gsumzmhm  18383  srgpcomp  18578  srgbinom  18591  lmodvsmmulgdi  18946  lmodsubdi  18968  rmodislmodlem  18978  0lmhm  19088  lspsneq  19170  qusrhm  19285  quscrng  19288  asclrhm  19390  resspsrmul  19465  evlsscasrng  19574  psropprmul  19656  evls1scasrng  19751  zringlpirlem3  19882  mulgrhm  19894  phssip  20051  frlmip  20165  frlmphl  20168  mat1ghm  20337  mat1mhm  20338  1marepvmarrepid  20429  mdetrlin  20456  mdetrsca2  20458  mdetunilem7  20472  mdetunilem9  20474  mndifsplit  20490  maducoeval2  20494  smadiadetglem2  20526  decpmatmul  20625  pm2mpghm  20669  pm2mpmhmlem2  20672  cpmidgsum2  20732  ptbasfi  21432  ptuni  21445  alexsubALTlem3  21900  subgtgp  21956  tsmsxplem1  22003  xmsusp  22421  restmetu  22422  nminv  22472  nrginvrcnlem  22542  copco  22864  pcoass  22870  pi1bas  22884  pi1xfrf  22899  pi1xfr  22901  isclmp  22943  cph2subdi  23056  cphassr  23058  tchcphlem1  23080  cphipval  23088  rrxip  23224  rrxnm  23225  pjthlem1  23254  ovolunlem1a  23310  ovolfs2  23385  uniiccdif  23392  ismbf  23442  itgaddlem2  23635  ditgswap  23668  ply1divex  23941  plyeq0lem  24011  plymullem1  24015  dgrcolem2  24075  vieta1lem2  24111  elqaalem2  24120  elqaalem3  24121  aaliou3lem7  24149  ulmshft  24189  mulcxplem  24475  cxpmul2  24480  root1eq1  24541  cxpeq  24543  logbchbase  24554  cosangneg2d  24582  isosctrlem2  24594  angpieqvdlem  24600  chordthmlem3  24606  chordthmlem4  24607  chordthmlem5  24608  quad2  24611  dcubic2  24616  cubic2  24620  quart1  24628  scvxcvx  24757  igamlgam  24821  lgam1  24835  basellem9  24860  ppifl  24931  mumul  24952  sgmmul  24971  chtublem  24981  chpub  24990  logfacrlim  24994  dchrsum2  25038  sumdchr2  25040  bposlem9  25062  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsdirnn0  25114  lgsdinn0  25115  lgsquad3  25157  2sqblem  25201  chpo1ub  25214  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2if  25231  dchrisum0fmul  25240  rpvmasum2  25246  mulog2sumlem1  25268  vmalogdivsum2  25272  log2sumbnd  25278  selberg3lem1  25291  selberg4lem1  25294  pntrsumo1  25299  selbergr  25302  pntpbnd1  25320  pntlemk  25340  tgbtwnconn1lem3  25514  mideulem2  25671  axlowdimlem16  25882  axcontlem8  25896  vtxval  25923  iedgval  25924  edgval  25986  vtxdgop  26422  finsumvtxdg2size  26502  clwlksfoclwwlk  27050  lp1cycl  27130  ex-ind-dvds  27448  vsfval  27616  lnocoi  27740  nmblolbii  27782  ipasslem5  27818  hvsubid  28011  sshjval3  28341  pjhthlem1  28378  adjval  28877  unopf1o  28903  kbpj  28943  lnopmi  28987  nmcoplbi  29015  cnlnadjlem2  29055  adjadd  29080  branmfn  29092  pjtoi  29166  ofoprabco  29592  xrsmulgzz  29806  archiabllem1a  29873  gsumvsca1  29910  gsumvsca2  29911  rdivmuldivd  29919  psgnfzto1stlem  29978  submat1n  29999  submatres  30000  madjusmdetlem3  30023  xrge0iifhom  30111  qqhval2lem  30153  qqhrhm  30161  qqhucn  30164  esumsnf  30254  measvunilem0  30404  carsgclctunlem1  30507  ballotlemfp1  30681  ballotlemsf1o  30703  signstfveq0  30782  breprexplemc  30838  breprexp  30839  breprexpnat  30840  circlemeth  30846  logdivsqrle  30856  hgt750lema  30863  cvmlift3lem2  31428  cvmlift3lem4  31430  cvmlift3lem5  31431  cvmlift3lem6  31432  cvmlift3lem9  31435  elmrsubrn  31543  bccolsum  31751  bj-bary1lem  33290  csbdif  33301  finixpnum  33524  poimirlem4  33543  poimirlem16  33555  poimirlem19  33558  poimirlem25  33564  mblfinlem3  33578  dvtan  33590  itg2addnc  33594  itgaddnclem2  33599  ftc1anclem6  33620  areacirclem5  33634  areacirc  33635  upixp  33654  prdsbnd2  33724  ismrer1  33767  rngoneglmul  33872  rngoisocnv  33910  islshpsm  34585  lshpnel2N  34590  lfl0f  34674  ldualvsdi1  34748  ldualgrplem  34750  cmtcomlemN  34853  cvlsupr8  34954  pmodl42N  35455  pmapjat1  35457  llnmod2i2  35467  dalawlem2  35476  pmapj2N  35533  idltrn  35754  cdlemc6  35801  cdleme20d  35917  cdleme22e  35949  cdleme22eALTN  35950  cdleme35b  36055  cdleme48fvg  36105  cdlemg4d  36218  cdlemg8a  36232  cdlemg42  36334  cdlemg47a  36339  tendodi1  36389  tendodi2  36390  cdlemk4  36439  cdlemk21N  36478  cdlemk22  36498  cdlemky  36531  cdlemk53b  36561  cdlemk53  36562  cdlemkyyN  36567  erngdvlem3-rN  36603  tendocnv  36627  dia1dim2  36668  dicvaddcl  36796  dihglblem3N  36901  dihmeetlem4preN  36912  dihmeet2  36952  lcfl7lem  37105  baerlem3lem1  37313  baerlem5alem1  37314  mapdh6bN  37343  mapdh6cN  37344  mapdh6dN  37345  hdmap1l6b  37418  hdmap1l6c  37419  hdmap1l6d  37420  hdmap14lem13  37489  pellexlem2  37711  rmxyneg  37802  oddcomabszz  37826  acongeq  37867  hausgraph  38107  fsovrfovd  38620  inductionexd  38770  expgrowth  38851  binomcxplemwb  38864  binomcxplemnn0  38865  binomcxplemnotnn0  38872  sumsnd  39499  restuni4  39618  fmuldfeqlem1  40132  cncfmptss  40137  climexp  40155  dvresntr  40450  stoweidlem17  40552  wallispi  40605  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem30  40672  fourierdlem41  40683  fourierdlem81  40722  fourierdlem103  40744  sge0xp  40964  sge0isummpt2  40967  isomennd  41066  vonioolem1  41215  sigarperm  41370  pwdif  41826  opoeALTV  41919  c0mgm  42234  c0mhm  42235  zrrnghm  42242  cznrng  42280  rngchomrnghmresALTV  42321  fdmdifeqresdif  42445  lincsum  42543  lincscm  42544  lmod1lem4  42604  blennngt2o2  42711  blennn0e2  42713  reccot  42827  rectan  42828  cotsqcscsq  42831  amgmlemALT  42877
  Copyright terms: Public domain W3C validator