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

Theorem 3eqtr2d 2691
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1 (𝜑𝐴 = 𝐵)
3eqtr2d.2 (𝜑𝐶 = 𝐵)
3eqtr2d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
3eqtr2d (𝜑𝐴 = 𝐷)

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr2d.2 . . 3 (𝜑𝐶 = 𝐵)
31, 2eqtr4d 2688 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2685 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:  fmptapd  6478  negsub  10367  neg2sub  10379  divmuleq  10768  divneg2  10787  discr  13041  bcpasc  13148  hashgval2  13205  hashf1lem2  13278  relexpaddnn  13835  crim  13899  remullem  13912  isum1p  14617  geo2sum  14648  fallfacfwd  14811  fsumkthpow  14831  bpoly3  14833  bpoly4  14834  efi4p  14911  sinhval  14928  addcos  14948  cos2tsin  14953  demoivreALT  14975  rpnnen2lem11  14997  omeo  15137  pwp1fsum  15161  sadaddlem  15235  bitsres  15242  smumullem  15261  sqgcd  15325  eulerthlem2  15534  vfermltlALT  15554  pockthlem  15656  4sqlem10  15698  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  fuccocl  16671  resssetc  16789  resscatc  16802  uncfcurf  16926  yonedalem3b  16966  prdspjmhm  17414  grpinvid2  17518  imasgrp2  17577  mulgaddcomlem  17610  mulgmodid  17628  lagsubg2  17702  cntzsubm  17814  sylow3lem2  18089  efgredleme  18202  ablsubsub  18269  ablsubsub4  18270  odadd2  18298  gex2abl  18300  pgpfac1lem3a  18521  abvneg  18882  lmodfopne  18949  lsppr  19141  psrass1  19453  resspsradd  19464  resspsrvsca  19466  mplcoe5  19516  mplmon2mul  19549  evlslem2  19560  evlsvarsrng  19576  coe1tm  19691  ply1scl1  19710  evls1varsrng  19752  gzrngunit  19860  frlmsubgval  20156  frlmgsum  20159  mamuass  20256  mavmulass  20403  mulmarep1gsum2  20428  mdetuni0  20475  maducoeval2  20494  madulid  20499  mat2pmatmul  20584  decpmatmulsumfsupp  20626  pmatcollpwlem  20633  pm2mpmhmlem1  20671  cmpfi  21259  cnconn  21273  txrest  21482  utopsnneiplem  22098  blcvx  22648  tchcphlem2  23081  cphipval2  23086  cphipval  23088  minveclem2  23243  pjthlem1  23254  uniioovol  23393  uniioombllem2  23397  itg1addlem4  23511  mbfi1fseqlem5  23531  itg2mulc  23559  itg2monolem1  23562  itgaddlem1  23634  itgmulc2lem2  23644  dvrec  23763  lhop2  23823  ftc1lem5  23848  deg1submon1p  23957  plypf1  24013  coefv0  24049  coemulhi  24055  coemulc  24056  dgreq0  24066  dvply1  24084  vieta1  24112  aareccl  24126  aaliou3lem8  24145  dvtaylp  24169  mtest  24203  sineq0  24318  efif1olem2  24334  efif1olem4  24336  tanarg  24410  logtayl2  24453  nnlogbexp  24564  isosctrlem2  24594  chordthmlem2  24605  chordthmlem4  24607  heron  24610  dcubic1lem  24615  dcubic1  24617  mcubic  24619  dquart  24625  quart1lem  24627  quart1  24628  efiasin  24660  asinsin  24664  atancj  24682  efiatan  24684  atanlogaddlem  24685  cosatan  24693  atantan  24695  atans2  24703  log2cnv  24716  log2tlbnd  24717  birthdaylem2  24724  cxplim  24743  lgamgulmlem2  24801  wilthlem1  24839  basellem3  24854  musum  24962  musumsum  24963  muinv  24964  pclogsum  24985  mersenne  24997  dchrabs  25030  dchrinv  25031  lgseisenlem1  25145  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2lem1  25154  2lgslem1  25164  chebbnd1lem3  25205  chpchtlim  25213  rplogsumlem2  25219  dchrisumlem2  25224  dchrmusum2  25228  mulog2sumlem1  25268  mulog2sumlem3  25270  vmalogdivsum2  25272  selberg4lem1  25294  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntibndlem2  25325  pntlemr  25336  pntlemf  25339  pntlemo  25341  ragcom  25638  colperpexlem1  25667  lmiisolem  25733  hypcgrlem2  25737  trgcopyeulem  25742  brbtwn2  25830  colinearalglem1  25831  colinearalglem2  25832  axcontlem2  25890  axcontlem8  25896  basvtxvalOLD  25948  numedglnl  26084  clwlkclwwlklem2a  26964  numclwwlk2  27361  numclwwlk2OLD  27368  grpoinvid2  27511  ablodivdiv4  27536  smcnlem  27680  ipidsq  27693  ipasslem2  27815  minvecolem2  27859  hv2times  28046  pjhthlem1  28378  pjds3i  28700  ho2times  28806  opsqrlem6  29132  pjclem4  29186  pj3si  29194  csmdsymi  29321  ofoprabco  29592  fcnvgreu  29600  2sqmod  29776  qqhcn  30163  esumpr2  30257  esumpfinval  30265  esumpfinvalf  30266  carsggect  30508  oddpwdcv  30545  eulerpartlemgs2  30570  fibp1  30591  orvcelval  30658  ballotlemscr  30708  ballotlemfrci  30717  signsplypnf  30755  reprpmtf1o  30832  breprexplemc  30838  breprexp  30839  circlemeth  30846  subfacp1lem5  31292  cvmliftlem10  31402  circum  31694  faclimlem3  31757  fwddifnp1  32397  bj-bary1lem  33290  tan2h  33531  poimirlem3  33542  poimirlem13  33552  poimirlem14  33553  itgaddnclem1  33598  itgmulc2nclem2  33607  areacirclem1  33630  areacirclem4  33633  istotbnd3  33700  iscringd  33927  3atlem1  35087  pmod2iN  35453  polval2N  35510  lhple  35646  cdleme2  35833  cdleme35d  36057  cdleme42h  36087  cdlemeg46ngfr  36123  cdlemkid1  36527  lcfl7lem  37105  mapdpglem22  37299  mapdh6dN  37345  hdmap1l6d  37420  hdmapinvlem3  37529  diophin  37653  irrapxlem2  37704  pellexlem6  37715  pell1234qrmulcl  37736  rmxyval  37797  rmxyneg  37802  rmxyadd  37803  jm2.24  37847  jm2.25  37883  snhesn  38397  radcnvrat  38830  binomcxplemnotnn0  38872  sub2times  39799  mul13d  39805  fperiodmullem  39831  fperiodmul  39832  isumneg  40152  climneg  40160  itgsinexp  40488  stoweidlem13  40548  stoweidlem42  40577  wallispilem4  40603  wallispilem5  40604  wallispi2lem1  40606  stirlinglem1  40609  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem7  40615  stirlinglem10  40618  dirkertrigeqlem3  40635  fourierdlem30  40672  fourierdlem32  40674  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem83  40724  sqwvfoura  40763  sqwvfourb  40764  etransclem2  40771  etransclem46  40815  sharhght  41375  fmtnorec3  41785  rngcid  42304  ringcid  42350  lmodvsmdi  42488  dmatALTbas  42515  ldepsprlem  42586  sinhpcosh  42809
  Copyright terms: Public domain W3C validator