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

Theorem 3eqtr4a 2496
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 2486 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2473 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  rabsnif  4072  uniintsn  4296  iinvdif  4374  iununi  4390  dmxpid  5074  rnxpid  5290  csbrn  5317  dmsnsnsn  5334  opswap  5343  xpcoid  5397  unizlim  5558  fvco4i  5959  fndmdifcom  6002  fmptsng  6100  fmptsnd  6101  csbov  6340  ordunisuc  6673  offres  6802  1stval2  6824  2ndval2  6825  cnvf1olem  6905  fparlem3  6909  fparlem4  6910  imacosupp  6966  seqomlem1  7175  ecovcom  7477  ecovass  7478  ecovdi  7479  resixpfo  7568  mapunen  7747  cardidm  8392  cardiun  8415  alephcard  8499  cardalephex  8519  cardcf  8680  cfidm  8703  alephsing  8704  itunisuc  8847  itunitc  8849  ituniiun  8850  alephadd  9000  alephreg  9005  pwcfsdom  9006  addcompq  9374  addcomnq  9375  mulcompq  9376  mulcomnq  9377  addassnq  9382  mulassnq  9383  addid1  9812  zeo  11021  xnegneg  11507  xaddcom  11531  xaddid1  11532  xnegdi  11534  xmulid1  11565  xadddilem  11580  ixxin  11652  fzsuc2  11851  expneg  12277  sq01  12391  facp1  12461  bcpasc  12503  hashf1lem1  12613  hashf1  12615  swrdccatin1  12824  swrdccat3blem  12836  repswsymballbi  12868  cshwmodn  12882  repswcshw  12896  trclun  13057  relexpcnv  13077  absexp  13346  sqreulem  13401  fsumf1o  13767  fsumadd  13783  fsumrev2  13821  fsumparts  13844  fsumrelem  13845  fprodf1o  13978  fprodmul  13992  fproddiv  13993  fprodfac  14005  fallfacfwd  14067  efexp  14133  tanval2  14165  sqr2irrlem  14278  sadeq  14420  smumullem  14440  smumul  14441  gcdcom  14458  gcd0id  14461  gcdass  14484  lcmcom  14528  lcmneg  14539  lcmass  14550  nn0gcdsq  14672  dfphi2  14691  pcneg  14786  setscom  15116  strfvi  15126  setsnid  15128  ressbas  15141  ressinbas  15147  ressress  15149  firest  15290  topnval  15292  xpsfeq  15421  xpsaddlem  15432  xpsvsca  15436  homffval  15546  oppchomfval  15570  oppcbas  15574  rescbas  15685  rescco  15688  cofuass  15745  fucbas  15816  fuchom  15817  setccatid  15930  estrccatid  15968  xpcbas  16014  xpchomfval  16015  xpccofval  16018  oduleval  16328  oduglb  16336  odulub  16338  ipotset  16354  grpinvfvi  16658  cntrval  16924  cntzval  16926  oppgplusfval  16950  symgbas  16972  symggrp  16992  pmtrprfval  17079  m1expaddsub  17090  sylow1lem2  17186  sylow3lem1  17214  oppglsm  17229  gsumzsplit  17495  gsum2dlem2  17538  gsumcom2  17542  dprd2dlem2  17608  dprd2da  17610  dmdprdsplit2lem  17613  mgpplusg  17662  mgpress  17669  ringidval  17672  opprmulfval  17788  abvtrivd  18003  sralem  18335  srasca  18339  sravsca  18340  sraip  18341  rlmval  18349  psrmulr  18543  mplmonmul  18623  mplcoe3  18625  opsrbaslem  18636  opsrtoslem2  18643  psr1val  18714  ply1basfvi  18769  ply1plusgfvi  18770  psr1sca2  18779  evl1fval1lem  18853  zlmlem  19019  zlmsca  19023  zlmvsca  19024  psgninv  19081  ocvval  19161  thlbas  19190  thlle  19191  thloc  19193  dsmmval2  19230  mattpos1  19412  mdettpos  19567  smadiadetglem1  19627  tgdif0  19939  indislem  19946  restco  20111  txtopon  20537  txindislem  20579  qtopres  20644  hmphindis  20743  ptuncnv  20753  snclseqg  21061  tsmssplit  21097  ussval  21205  tuslem  21213  setsmsbas  21421  tnglem  21579  tngds  21587  tngtset  21588  pcoass  21948  cphsqrtcl2  22057  rrxcph  22244  ovolunlem1a  22327  ioorinv  22405  ioorinvOLD  22410  itg11  22526  itg1mulc  22539  itg2cnlem1  22596  iblss2  22640  ibladdlem  22654  itgfsum  22661  iblabslem  22662  iblabs  22663  ditgneg  22689  deg1fvi  22911  dgrco  23097  logfac  23415  cxpexp  23478  cxpmul2  23499  cxpsqrt  23513  dvcxp1  23545  dvcxp2  23546  ang180lem1  23603  mcubic  23638  quart1  23647  reasinsin  23687  atanlogaddlem  23704  atantayl2  23729  log2tlbnd  23736  basellem2  23871  basellem3  23872  basellem5  23874  basellem8  23877  dchrmulid2  24043  bcp1ctr  24070  lgsneg  24110  lgsneg1  24111  lgsdir2  24119  lgsdir  24121  lgsdi  24123  lgsquad2lem2  24150  pntleml  24312  motgrp  24448  lmiisolem  24694  ttglem  24752  eupath2lem3  25552  bafval  26068  ipidsq  26194  ipasslem1  26317  pjclem2  27684  cvmdi  27812  imadifxp  28051  iundisjcnt  28210  resvsca  28432  indval2  28675  bayesth  29098  plymulx  29225  subfacp1lem6  29696  mvtval  29926  mexval  29928  mexval2  29929  mdvval  29930  mrsubfval  29934  mrsubvrs  29948  msubfval  29950  elmsubrn  29954  mvhfval  29959  mpstval  29961  msrfval  29963  mstaval  29970  mthmval  30001  bccolsum  30162  dfrdg2  30229  dfrdg3  30230  dfrdg4  30503  ordtoplem  30880  ordcmp  30892  poimirlem6  31649  poimirlem7  31650  poimirlem11  31654  poimirlem12  31655  poimirlem13  31656  poimirlem14  31657  poimirlem16  31659  poimirlem19  31662  poimirlem21  31664  poimirlem22  31665  poimirlem27  31670  poimirlem31  31674  poimirlem32  31675  mblfinlem2  31681  itg2addnclem2  31697  ibladdnclem  31701  iblabsnclem  31708  iblabsnc  31709  iblmulc2nc  31710  ftc1anclem8  31727  pmodN  33123  tgrpgrplem  34024  tendoplass  34058  tendoicl  34071  erngdvlem3  34265  dvhvaddass  34373  dib0  34440  dib1dim2  34444  diclspsn  34470  cdlemn8  34480  dihopelvalcpre  34524  djhcom  34681  kelac2  35628  mendbas  35748  mendsca  35753  mendring  35756  relexp01min  35943  relexpaddss  35948  iotain  36404  addrcom  36464  itgsinexplem1  37398  volioc  37417  dirkertrigeqlem1  37528  fourierdlem104  37641  sqwvfoura  37659  sqwvfourb  37660  fzopredsuc  38109  rngccatidALTV  38748  ringccatidALTV  38811  0dig2pr01  39181  nn0sumshdiglemB  39191  dpfrac1  39252
  Copyright terms: Public domain W3C validator