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

Theorem 3eqtr4a 2494
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 2484 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2471 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  uniintsn  4087  iununi  4175  unizlim  4698  ordunisuc  4812  dmxpid  5089  rnxpid  5302  dmsnsnsn  5348  opswap  5356  xpcoid  5415  fvco4i  5801  fndmdifcom  5835  offres  6319  1stval2  6364  2ndval2  6365  cnvf1olem  6444  fparlem3  6448  fparlem4  6449  seqomlem1  6707  ecovcom  7015  ecovass  7016  ecovdi  7017  resixpfo  7100  mapunen  7276  cardidm  7846  cardiun  7869  alephcard  7951  cardalephex  7971  cardcf  8132  cfidm  8155  alephsing  8156  itunisuc  8299  itunitc  8301  ituniiun  8302  alephadd  8452  alephreg  8457  pwcfsdom  8458  addcompq  8827  addcomnq  8828  mulcompq  8829  mulcomnq  8830  addassnq  8835  mulassnq  8836  addid1  9246  zeo  10355  xnegneg  10800  xaddcom  10824  xaddid1  10825  xnegdi  10827  xmulid1  10858  xadddilem  10873  ixxin  10933  fzsuc2  11104  expneg  11389  sq01  11501  facp1  11571  bcpasc  11612  hashf1lem1  11704  hashf1  11706  eqs1  11761  absexp  12109  sqreulem  12163  fsumf1o  12517  fsumadd  12532  fsumrev2  12565  fsumparts  12585  fsumrelem  12586  efexp  12702  tanval2  12734  sqr2irrlem  12847  sadeq  12984  smumullem  13004  smumul  13005  gcdcom  13020  gcd0id  13023  gcdass  13045  nn0gcdsq  13144  dfphi2  13163  pcneg  13247  setscom  13497  strfvi  13507  setsnid  13509  ressbas  13519  ressinbas  13525  ressress  13526  firest  13660  topnval  13662  xpsfeq  13789  xpsaddlem  13800  xpsvsca  13804  homffval  13917  oppchomfval  13940  oppcbas  13944  rescbas  14029  rescco  14032  cofuass  14086  fucbas  14157  fuchom  14158  setccatid  14239  xpcbas  14275  xpchomfval  14276  xpccofval  14279  oduleval  14558  oduglb  14566  odulub  14568  ipotset  14583  grpinvfvi  14846  symgbas  15095  symggrp  15103  cntrval  15118  cntzval  15120  oppgplusfval  15144  sylow1lem2  15233  sylow3lem1  15261  oppglsm  15276  gsumzsplit  15529  gsum2d  15546  gsumcom2  15549  dprd2dlem2  15598  dprd2da  15600  dmdprdsplit2lem  15603  mgpplusg  15652  mgpress  15659  rngidval  15666  opprmulfval  15730  abvtrivd  15928  sralem  16249  srasca  16253  sravsca  16254  rlmval  16264  psrmulr  16448  mplmonmul  16527  mplcoe3  16529  opsrbaslem  16538  opsrtoslem2  16545  psr1val  16584  ply1basfvi  16635  ply1plusgfvi  16636  psr1sca2  16645  zlmlem  16798  zlmsca  16802  zlmvsca  16803  ocvval  16894  thlbas  16923  thlle  16924  thloc  16926  tgdif0  17057  indislem  17064  restco  17228  txtopon  17623  txindislem  17665  qtopres  17730  hmphindis  17829  ptuncnv  17839  snclseqg  18145  tsmssplit  18181  ussval  18289  tuslem  18297  setsmsbas  18505  tnglem  18681  tngds  18689  tngtset  18690  pcoass  19049  cphsqrcl2  19149  ovolunlem1a  19392  ioorinv  19468  itg11  19583  itg1mulc  19596  itg2cnlem1  19653  iblss2  19697  ibladdlem  19711  itgfsum  19718  iblabslem  19719  iblabs  19720  ditgneg  19744  deg1fvi  20008  dgrco  20193  logfac  20495  cxpexp  20559  cxpmul2  20580  cxpsqr  20594  dvcxp2  20627  ang180lem1  20651  mcubic  20687  quart1  20696  reasinsin  20736  atanlogaddlem  20753  atantayl2  20778  log2tlbnd  20785  basellem2  20864  basellem3  20865  basellem5  20867  basellem8  20870  dchrmulid2  21036  bcp1ctr  21063  lgsneg  21103  lgsneg1  21104  lgsdir2  21112  lgsdir  21114  lgsdi  21116  lgsquad2lem2  21143  pntleml  21305  eupath2lem3  21701  bafval  22083  ipidsq  22209  ipasslem1  22332  pjclem2  23699  cvmdi  23827  imadifxp  24038  iundisjcnt  24154  indval2  24412  sitgclcn  24658  sitgclre  24659  bayesth  24697  subfacp1lem6  24871  fprodf1o  25272  fprodmul  25284  fproddiv  25285  fprodfac  25296  fallfacfwd  25352  dfrdg2  25423  dfrdg3  25424  dfrdg4  25795  ordtoplem  26185  ordcmp  26197  mblfinlem2  26244  itg2addnclem2  26257  ibladdnclem  26261  iblabsnclem  26268  iblabsnc  26269  iblmulc2nc  26270  ftc1anclem8  26287  kelac2  27140  dsmmval2  27179  m1expaddsub  27398  mendbas  27469  mendsca  27474  mendrng  27477  iotain  27594  addrcom  27656  itgsinexplem1  27724  swrdccatin1  28205  swrdccat3blem  28218  dpfrac1  28515  pmodN  30647  tgrpgrplem  31546  tendoplass  31580  tendoicl  31593  erngdvlem3  31787  dvhvaddass  31895  dib0  31962  dib1dim2  31966  diclspsn  31992  cdlemn8  32002  dihopelvalcpre  32046  djhcom  32203
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator