Theorem 3eqtr4a 2882

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	⊢ 𝐴 = 𝐵
3eqtr4a.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4a.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	syl6eq 2872	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2859	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  rabsnif  4658  uniintsn  4912  iinvdif  5001  iununi  5020  dmxpid  5799  rnxpid  6029  csbrn  6059  dmsnsnsn  6076  opswap  6085  xpcoid  6140  unizlim  6306  fvco4i  6761  fndmdifcom  6812  fmptsng  6929  fmptsnd  6930  csbov  7198  ordunisuc  7546  offres  7683  1stval2  7705  2ndval2  7706  cnvf1olem  7804  fparlem3  7808  fparlem4  7809  imacosuppOLD  7874  seqomlem1  8085  ecovcom  8402  ecovass  8403  ecovdi  8404  resixpfo  8499  mapunen  8685  cardidm  9387  cardiun  9410  alephcard  9495  cardalephex  9515  cardcf  9673  cfidm  9696  alephsing  9697  itunisuc  9840  itunitc  9842  ituniiun  9843  alephadd  9998  alephreg  10003  pwcfsdom  10004  addcompq  10371  addcomnq  10372  mulcompq  10373  mulcomnq  10374  addassnq  10379  mulassnq  10380  addid1  10819  zeo  12067  xnegneg  12606  xaddcom  12632  xaddid1  12633  xnegdi  12640  xmulid1  12671  xadddilem  12686  ixxin  12754  fzsuc2  12964  expneg  13436  sq01  13585  facp1  13637  bcpasc  13680  hashfzp1  13791  resunimafz0  13802  hashf1lem1  13812  hashf1  13814  ccat1st1st  13983  swrdccatin1  14086  swrdccat3blem  14100  repswsymballbi  14141  cshwmodn  14156  cshwlen  14160  repswcshw  14173  trclun  14373  relexpcnv  14393  absexp  14663  sqreulem  14718  fsumf1o  15079  fsumadd  15095  fsumrev2  15136  fsumparts  15160  fsumrelem  15161  pwm1geoserOLD  15224  fprodf1o  15299  fprodmul  15313  fproddiv  15314  fprodfac  15326  fallfacfwd  15389  efexp  15453  tanval2  15485  sadeq  15820  smumullem  15840  smumul  15841  gcdcom  15861  gcd0id  15866  gcdass  15894  lcmcom  15936  lcmneg  15946  lcmass  15957  nn0gcdsq  16091  dfphi2  16110  pcneg  16209  setscom  16526  strfvi  16536  setsnid  16538  ressbas  16553  ressinbas  16559  ressress  16561  firest  16705  topnval  16707  xpsfeq  16835  xpsaddlem  16845  xpsvsca  16849  oppchomfval  16983  oppcbas  16987  rescbas  17098  rescco  17101  cofuass  17158  fucbas  17229  fuchom  17230  setccatid  17343  estrccatid  17381  xpcbas  17427  oduleval  17740  oduglb  17748  odulub  17750  ipotset  17766  efmndbas  18035  efmndbasabf  18036  symggrplem  18048  smndex1mndlem  18073  pwmnd  18101  grpinvfvi  18145  cntrval  18448  cntzval  18450  oppgplusfval  18475  snsymgefmndeq  18522  symgvalstruct  18524  pmtrprfval  18614  m1expaddsub  18625  sylow1lem2  18723  sylow3lem1  18751  oppglsm  18766  gsumzsplit  19046  gsum2dlem2  19090  gsumcom2  19094  dprd2dlem2  19161  dprd2da  19163  dmdprdsplit2lem  19166  mgpplusg  19242  mgpress  19249  ringidval  19252  opprmulfval  19374  abvtrivd  19610  sralem  19948  srasca  19952  sravsca  19953  sraip  19954  rlmval  19962  psrmulr  20163  mplmonmul  20244  mplcoe3  20246  opsrbaslem  20257  opsrtoslem2  20264  psr1val  20353  ply1basfvi  20408  ply1plusgfvi  20409  psr1sca2  20418  evl1fval1lem  20492  zlmlem  20663  zlmsca  20667  zlmvsca  20668  psgninv  20725  ocvval  20810  thlbas  20839  thlle  20840  thloc  20842  dsmmval2  20879  mattpos1  21064  mdettpos  21219  smadiadetglem1  21279  tgdif0  21599  indislem  21607  restco  21771  txtopon  22198  txindislem  22240  qtopres  22305  hmphindis  22404  ptuncnv  22414  snclseqg  22723  tsmssplit  22759  ussval  22867  tuslem  22875  setsmsbas  23084  tnglem  23248  tngds  23256  tngtset  23257  pcoass  23627  cphsqrtcl2  23789  rrxcph  23994  ovolunlem1a  24096  ioorinv  24176  itg11  24291  itg1mulc  24304  itg2cnlem1  24361  iblss2  24405  ibladdlem  24419  itgfsum  24426  iblabslem  24427  iblabs  24428  ditgneg  24454  deg1fvi  24678  dgrco  24864  logfac  25183  cxpexp  25250  cxpmul2  25271  cxpsqrt  25285  cxpsqrtth  25311  dvcxp1  25320  dvcxp2  25321  ang180lem1  25386  mcubic  25424  quart1  25433  reasinsin  25473  atanlogaddlem  25490  atantayl2  25515  log2tlbnd  25522  basellem2  25658  basellem3  25659  basellem5  25661  basellem8  25664  dchrmulid2  25827  bcp1ctr  25854  lgsneg  25896  lgsneg1  25897  lgsdir2  25905  lgsdir  25907  lgsdi  25909  lgsquad2lem2  25960  pntleml  26186  motgrp  26328  lmiisolem  26581  ttglem  26661  egrsubgr  27058  iswwlksnon  27630  iswspthsnon  27633  bafval  28380  ipidsq  28486  ipasslem1  28607  pjclem2  29972  cvmdi  30100  imadifxp  30350  iundisjcnt  30520  dpfrac1  30568  cycpmco2rn  30767  cyc3genpmlem  30793  resvsca  30903  indval2  31273  bayesth  31697  ofcccat  31813  plymulx  31818  subfacp1lem6  32432  satfdm  32616  mvtval  32747  mexval  32749  mexval2  32750  mdvval  32751  mrsubfval  32755  mrsubvrs  32769  msubfval  32771  elmsubrn  32775  mvhfval  32780  mpstval  32782  msrfval  32784  mstaval  32791  mthmval  32822  bccolsum  32971  dfrdg2  33040  dfrdg3  33041  frrlem12  33134  dfrdg4  33412  ordtoplem  33783  ordcmp  33795  curunc  34873  matunitlindflem2  34888  poimirlem6  34897  poimirlem7  34898  poimirlem11  34902  poimirlem12  34903  poimirlem13  34904  poimirlem14  34905  poimirlem16  34907  poimirlem19  34910  poimirlem21  34912  poimirlem22  34913  poimirlem27  34918  poimirlem31  34922  poimirlem32  34923  itg2addnclem2  34943  ibladdnclem  34947  iblabsnclem  34954  iblabsnc  34955  iblmulc2nc  34956  ftc1anclem8  34973  pmodN  36985  tgrpgrplem  37884  tendoplass  37918  tendoicl  37931  erngdvlem3  38125  dvhvaddass  38232  dib0  38299  dib1dim2  38303  diclspsn  38329  cdlemn8  38339  dihopelvalcpre  38383  djhcom  38540  nn0expgcd  39182  kelac2  39663  mendbas  39782  mendsca  39787  mendring  39790  iscard4  39898  relexp01min  40056  relexpaddss  40061  iotain  40747  addrcom  40805  rnsnf  41442  itgsinexplem1  42237  volioc  42255  dirkertrigeqlem1  42382  fourierdlem104  42494  sqwvfoura  42512  sqwvfourb  42513  fzopredsuc  43522  fppr2odd  43895  rngccatidALTV  44259  ringccatidALTV  44322  0dig2pr01  44669  nn0sumshdiglemB  44679