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

Theorem 3eqtr4a 2522
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1  |-  A  =  B
3eqtr4a.2  |-  ( ph  ->  C  =  A )
3eqtr4a.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3  |-  ( ph  ->  C  =  A )
2 3eqtr4a.1 . . 3  |-  A  =  B
31, 2syl6eq 2512 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2499 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  rabsnif  4054  uniintsn  4286  iinvdif  4364  iununi  4382  dmxpid  5076  rnxpid  5292  csbrn  5320  dmsnsnsn  5337  opswap  5346  xpcoid  5400  unizlim  5562  fvco4i  5971  fndmdifcom  6015  fmptsng  6114  fmptsnd  6115  csbov  6355  ordunisuc  6691  offres  6820  1stval2  6842  2ndval2  6843  cnvf1olem  6926  fparlem3  6930  fparlem4  6931  imacosupp  6987  seqomlem1  7198  ecovcom  7500  ecovass  7501  ecovdi  7502  resixpfo  7591  mapunen  7772  cardidm  8424  cardiun  8447  alephcard  8532  cardalephex  8552  cardcf  8713  cfidm  8736  alephsing  8737  itunisuc  8880  itunitc  8882  ituniiun  8883  alephadd  9033  alephreg  9038  pwcfsdom  9039  addcompq  9406  addcomnq  9407  mulcompq  9408  mulcomnq  9409  addassnq  9414  mulassnq  9415  addid1  9844  zeo  11055  xnegneg  11541  xaddcom  11565  xaddid1  11566  xnegdi  11568  xmulid1  11599  xadddilem  11614  ixxin  11686  fzsuc2  11888  expneg  12318  sq01  12432  facp1  12502  bcpasc  12544  hashf1lem1  12657  hashf1  12659  swrdccatin1  12882  swrdccat3blem  12894  repswsymballbi  12926  cshwmodn  12940  repswcshw  12954  trclun  13133  relexpcnv  13153  absexp  13422  sqreulem  13477  fsumf1o  13844  fsumadd  13860  fsumrev2  13898  fsumparts  13921  fsumrelem  13922  fprodf1o  14055  fprodmul  14069  fproddiv  14070  fprodfac  14082  fallfacfwd  14144  efexp  14210  tanval2  14242  sqr2irrlem  14355  sadeq  14501  smumullem  14521  smumul  14522  gcdcom  14539  gcd0id  14542  gcdass  14568  lcmcom  14612  lcmneg  14623  lcmass  14634  nn0gcdsq  14756  dfphi2  14777  pcneg  14878  setscom  15208  strfvi  15218  setsnid  15220  ressbas  15234  ressinbas  15240  ressress  15242  firest  15386  topnval  15388  xpsfeq  15525  xpsaddlem  15536  xpsvsca  15540  homffval  15650  oppchomfval  15674  oppcbas  15678  rescbas  15789  rescco  15792  cofuass  15849  fucbas  15920  fuchom  15921  setccatid  16034  estrccatid  16072  xpcbas  16118  xpchomfval  16119  xpccofval  16122  oduleval  16432  oduglb  16440  odulub  16442  ipotset  16458  grpinvfvi  16762  cntrval  17028  cntzval  17030  oppgplusfval  17054  symgbas  17076  symggrp  17096  pmtrprfval  17183  m1expaddsub  17194  sylow1lem2  17306  sylow3lem1  17334  oppglsm  17349  gsumzsplit  17615  gsum2dlem2  17658  gsumcom2  17662  dprd2dlem2  17728  dprd2da  17730  dmdprdsplit2lem  17733  mgpplusg  17782  mgpress  17789  ringidval  17792  opprmulfval  17908  abvtrivd  18123  sralem  18455  srasca  18459  sravsca  18460  sraip  18461  rlmval  18469  psrmulr  18663  mplmonmul  18743  mplcoe3  18745  opsrbaslem  18756  opsrtoslem2  18763  psr1val  18834  ply1basfvi  18889  ply1plusgfvi  18890  psr1sca2  18899  evl1fval1lem  18973  zlmlem  19143  zlmsca  19147  zlmvsca  19148  psgninv  19205  ocvval  19285  thlbas  19314  thlle  19315  thloc  19317  dsmmval2  19354  mattpos1  19536  mdettpos  19691  smadiadetglem1  19751  tgdif0  20063  indislem  20070  restco  20235  txtopon  20661  txindislem  20703  qtopres  20768  hmphindis  20867  ptuncnv  20877  snclseqg  21185  tsmssplit  21221  ussval  21329  tuslem  21337  setsmsbas  21545  tnglem  21703  tngds  21711  tngtset  21712  pcoass  22110  cphsqrtcl2  22219  rrxcph  22406  ovolunlem1a  22504  ioorinv  22584  ioorinvOLD  22589  itg11  22705  itg1mulc  22718  itg2cnlem1  22775  iblss2  22819  ibladdlem  22833  itgfsum  22840  iblabslem  22841  iblabs  22842  ditgneg  22868  deg1fvi  23090  dgrco  23285  logfac  23606  cxpexp  23669  cxpmul2  23690  cxpsqrt  23704  dvcxp1  23736  dvcxp2  23737  ang180lem1  23794  mcubic  23829  quart1  23838  reasinsin  23878  atanlogaddlem  23895  atantayl2  23920  log2tlbnd  23927  basellem2  24064  basellem3  24065  basellem5  24067  basellem8  24070  dchrmulid2  24236  bcp1ctr  24263  lgsneg  24303  lgsneg1  24304  lgsdir2  24312  lgsdir  24314  lgsdi  24316  lgsquad2lem2  24343  pntleml  24505  motgrp  24644  lmiisolem  24894  ttglem  24962  eupath2lem3  25763  bafval  26279  ipidsq  26405  ipasslem1  26528  pjclem2  27905  cvmdi  28033  imadifxp  28265  iundisjcnt  28426  resvsca  28644  indval2  28887  bayesth  29322  plymulx  29487  subfacp1lem6  29958  mvtval  30188  mexval  30190  mexval2  30191  mdvval  30192  mrsubfval  30196  mrsubvrs  30210  msubfval  30212  elmsubrn  30216  mvhfval  30221  mpstval  30223  msrfval  30225  mstaval  30232  mthmval  30263  bccolsum  30425  dfrdg2  30492  dfrdg3  30493  dfrdg4  30768  ordtoplem  31145  ordcmp  31157  poimirlem6  31992  poimirlem7  31993  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem16  32002  poimirlem19  32005  poimirlem21  32007  poimirlem22  32008  poimirlem27  32013  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  itg2addnclem2  32040  ibladdnclem  32044  iblabsnclem  32051  iblabsnc  32052  iblmulc2nc  32053  ftc1anclem8  32070  pmodN  33461  tgrpgrplem  34362  tendoplass  34396  tendoicl  34409  erngdvlem3  34603  dvhvaddass  34711  dib0  34778  dib1dim2  34782  diclspsn  34808  cdlemn8  34818  dihopelvalcpre  34862  djhcom  35019  kelac2  35969  mendbas  36096  mendsca  36101  mendring  36104  relexp01min  36351  relexpaddss  36356  iotain  36813  addrcom  36873  itgsinexplem1  37916  volioc  37935  dirkertrigeqlem1  38061  fourierdlem104  38175  sqwvfoura  38193  sqwvfourb  38194  fzopredsuc  38855  opidg  39134  egrsubgr  39495  rngccatidALTV  40360  ringccatidALTV  40423  0dig2pr01  40790  nn0sumshdiglemB  40800  dpfrac1  40861
  Copyright terms: Public domain W3C validator