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

Theorem 3eqtr2d 2649
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 2646 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2643 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  fmptapd  6320  negsub  10180  neg2sub  10192  divmuleq  10579  divneg2  10598  discr  12818  bcpasc  12925  hashgval2  12980  hashf1lem2  13049  relexpaddnn  13585  crim  13649  remullem  13662  isum1p  14358  geo2sum  14389  fallfacfwd  14552  fsumkthpow  14572  bpoly3  14574  bpoly4  14575  efi4p  14652  sinhval  14669  addcos  14689  cos2tsin  14694  demoivreALT  14716  rpnnen2lem11  14738  omeo  14874  pwp1fsum  14898  sadaddlem  14972  bitsres  14979  smumullem  14998  sqgcd  15062  eulerthlem2  15271  vfermltlALT  15291  pockthlem  15393  4sqlem10  15435  vdwlem2  15470  vdwlem6  15474  vdwlem8  15476  fuccocl  16393  resssetc  16511  resscatc  16524  uncfcurf  16648  yonedalem3b  16688  prdspjmhm  17136  grpinvid2  17240  imasgrp2  17299  mulgaddcomlem  17332  mulgmodid  17350  lagsubg2  17424  cntzsubm  17537  sylow3lem2  17812  efgredleme  17925  ablsubsub  17992  ablsubsub4  17993  odadd2  18021  gex2abl  18023  pgpfac1lem3a  18244  abvneg  18603  lmodfopne  18670  lsppr  18860  psrass1  19172  resspsradd  19183  resspsrvsca  19185  mplcoe5  19235  mplmon2mul  19268  evlslem2  19279  evlsvarsrng  19295  coe1tm  19410  ply1scl1  19429  evls1varsrng  19471  gzrngunit  19577  frlmsubgval  19869  frlmgsum  19872  mamuass  19969  mavmulass  20116  mulmarep1gsum2  20141  mdetuni0  20188  maducoeval2  20207  madulid  20212  mat2pmatmul  20297  decpmatmulsumfsupp  20339  pmatcollpwlem  20346  pm2mpmhmlem1  20384  cmpfi  20963  cnconn  20977  txrest  21186  utopsnneiplem  21803  blcvx  22341  tchcphlem2  22764  minveclem2  22922  pjthlem1  22933  uniioovol  23070  uniioombllem2  23074  itg1addlem4  23189  mbfi1fseqlem5  23209  itg2mulc  23237  itg2monolem1  23240  itgaddlem1  23312  itgmulc2lem2  23322  dvrec  23441  lhop2  23499  ftc1lem5  23524  deg1submon1p  23633  plypf1  23689  coefv0  23725  coemulhi  23731  coemulc  23732  dgreq0  23742  dvply1  23760  vieta1  23788  aareccl  23802  aaliou3lem8  23821  dvtaylp  23845  mtest  23879  sineq0  23994  efif1olem2  24010  efif1olem4  24012  tanarg  24086  logtayl2  24125  nnlogbexp  24236  isosctrlem2  24266  chordthmlem2  24277  chordthmlem4  24279  heron  24282  dcubic1lem  24287  dcubic1  24289  mcubic  24291  dquart  24297  quart1lem  24299  quart1  24300  efiasin  24332  asinsin  24336  atancj  24354  efiatan  24356  atanlogaddlem  24357  cosatan  24365  atantan  24367  atans2  24375  log2cnv  24388  log2tlbnd  24389  birthdaylem2  24396  cxplim  24415  lgamgulmlem2  24473  wilthlem1  24511  basellem3  24526  musum  24634  musumsum  24635  muinv  24636  pclogsum  24657  mersenne  24669  dchrabs  24702  dchrinv  24703  lgseisenlem1  24817  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  lgsquad2lem1  24826  2lgslem1  24836  chebbnd1lem3  24877  chpchtlim  24885  rplogsumlem2  24891  dchrisumlem2  24896  dchrmusum2  24900  mulog2sumlem1  24940  mulog2sumlem3  24942  vmalogdivsum2  24944  selberg4lem1  24966  pntrlog2bndlem2  24984  pntrlog2bndlem4  24986  pntibndlem2  24997  pntlemr  25008  pntlemf  25011  pntlemo  25013  ragcom  25311  colperpexlem1  25340  lmiisolem  25406  hypcgrlem2  25410  trgcopyeulem  25415  brbtwn2  25503  colinearalglem1  25504  colinearalglem2  25505  axcontlem2  25563  axcontlem8  25569  clwlkisclwwlklem2a  26079  numclwwlk2  26400  grpoinvid2  26533  ablodivdiv4  26561  vcoprneOLD  26600  nvnncan  26688  smcnlem  26737  ipidsq  26753  ipasslem2  26877  minvecolem2  26921  hv2times  27108  pjhthlem1  27440  pjds3i  27762  ho2times  27868  opsqrlem6  28194  pjclem4  28248  pj3si  28256  csmdsymi  28383  ofoprabco  28653  fcnvgreu  28661  2sqmod  28785  qqhcn  29169  esumpr2  29262  esumpfinval  29270  esumpfinvalf  29271  carsggect  29513  oddpwdcv  29550  eulerpartlemgs2  29575  fibp1  29596  orvcelval  29663  ballotlemscr  29713  ballotlemfrci  29722  signsplypnf  29759  subfacp1lem5  30226  cvmliftlem10  30336  circum  30628  faclimlem3  30690  fwddifnp1  31248  bj-bary1lem  32133  tan2h  32367  poimirlem3  32378  poimirlem13  32388  poimirlem14  32389  itgaddnclem1  32434  itgmulc2nclem2  32443  areacirclem1  32466  areacirclem4  32469  istotbnd3  32536  iscringd  32763  3atlem1  33583  pmod2iN  33949  polval2N  34006  lhple  34142  cdleme2  34329  cdleme35d  34554  cdleme42h  34584  cdlemeg46ngfr  34620  cdlemkid1  35024  lcfl7lem  35602  mapdpglem22  35796  mapdh6dN  35842  hdmap1l6d  35917  hdmapinvlem3  36026  diophin  36150  irrapxlem2  36201  pellexlem6  36212  pell1234qrmulcl  36233  rmxyval  36294  rmxyneg  36299  rmxyadd  36300  jm2.24  36344  jm2.25  36380  snhesn  36896  radcnvrat  37331  binomcxplemnotnn0  37373  sub2times  38222  mul13d  38228  fperiodmullem  38254  fperiodmul  38255  isumneg  38466  climneg  38474  itgsinexp  38643  stoweidlem13  38703  stoweidlem42  38732  wallispilem4  38758  wallispilem5  38759  wallispi2lem1  38761  stirlinglem1  38764  stirlinglem3  38766  stirlinglem4  38767  stirlinglem5  38768  stirlinglem7  38770  stirlinglem10  38773  dirkertrigeqlem3  38790  fourierdlem30  38827  fourierdlem32  38829  fourierdlem42  38839  fourierdlem48  38844  fourierdlem49  38845  fourierdlem83  38879  sqwvfoura  38918  sqwvfourb  38919  etransclem2  38926  etransclem46  38970  sharhght  39500  fmtnorec3  39796  basvtxval  40244  clwlkclwwlklem2a  41202  av-numclwwlk2  41532  rngcid  41766  ringcid  41812  lmodvsmdi  41952  dmatALTbas  41979  ldepsprlem  42050  sinhpcosh  42236
  Copyright terms: Public domain W3C validator