Theorem 3eqtr4a 2792

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	eqtrdi 2782	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2769	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  rabsnif  4673  uniintsn  4933  iinvdif  5026  iununi  5045  dmxpid  5869  rnxpid  6120  csbrn  6150  dmsnsnsn  6167  opswap  6176  xpcoid  6237  predres  6286  unizlim  6430  fvco4i  6923  fndmdifcom  6976  fmptsng  7102  fmptsnd  7103  csbov  7391  ordunisuc  7762  offres  7915  1stval2  7938  2ndval2  7939  cnvf1olem  8040  fparlem3  8044  fparlem4  8045  frrlem12  8227  seqomlem1  8369  ecovcom  8747  ecovass  8748  ecovdi  8749  resixpfo  8860  mapunen  9059  cardidm  9852  cardiun  9875  alephcard  9961  cardalephex  9981  cardcf  10143  cfidm  10166  alephsing  10167  itunisuc  10310  itunitc  10312  ituniiun  10313  alephadd  10468  alephreg  10473  pwcfsdom  10474  addcompq  10841  addcomnq  10842  mulcompq  10843  mulcomnq  10844  addassnq  10849  mulassnq  10850  addrid  11293  zeo  12559  xnegneg  13113  xaddcom  13139  xaddrid  13140  xnegdi  13147  xmulrid  13178  xadddilem  13193  ixxin  13262  fzsuc2  13482  expneg  13976  sq01  14132  facp1  14185  bcpasc  14228  hashfzp1  14338  resunimafz0  14352  hashf1lem1  14362  hashf1  14364  ccat1st1st  14536  swrdccatin1  14632  swrdccat3blem  14646  repswsymballbi  14687  cshwmodn  14702  cshwlen  14706  repswcshw  14719  trclun  14921  relexpcnv  14942  relexpaddd  14961  absexp  15211  sqreulem  15267  fsumf1o  15630  fsumadd  15647  fsumrev2  15689  fsumparts  15713  fsumrelem  15714  fprodf1o  15853  fprodmul  15867  fproddiv  15868  fprodfac  15880  fallfacfwd  15943  efexp  16010  tanval2  16042  sadeq  16383  smumullem  16403  smumul  16404  gcdcom  16424  gcd0id  16430  gcdass  16458  nn0expgcd  16475  lcmcom  16504  lcmneg  16514  lcmass  16525  nn0gcdsq  16663  dfphi2  16685  pcneg  16786  setscom  17091  strfvi  17101  fveqprc  17102  oveqprc  17103  ressbas  17147  ressinbas  17156  ressress  17158  firest  17336  topnval  17338  xpsfeq  17467  xpsaddlem  17477  xpsvsca  17481  oppchomfval  17620  rescbas  17736  rescco  17739  cofuass  17796  fucbas  17870  fuchom  17871  setccatid  17991  estrccatid  18038  xpcbas  18084  oduleval  18195  odulub  18311  oduglb  18313  ipotset  18439  efmndbas  18779  efmndbasabf  18780  symggrplem  18792  smndex1mndlem  18817  pwmnd  18845  grpinvfvi  18895  cntrval  19231  cntzval  19233  oppgplusfval  19260  snsymgefmndeq  19307  symgvalstruct  19309  pmtrprfval  19399  m1expaddsub  19410  sylow1lem2  19511  sylow3lem1  19539  oppglsm  19554  gsumzsplit  19839  gsum2dlem2  19883  gsumcom2  19887  dprd2dlem2  19954  dprd2da  19956  dmdprdsplit2lem  19959  mgpplusg  20062  mgpress  20068  ringidval  20101  opprmulfval  20257  abvtrivd  20747  sralem  21110  srasca  21114  sravsca  21115  sraip  21116  rlmval  21125  zlmsca  21457  zlmvsca  21458  psgninv  21519  ocvval  21604  thlbas  21633  thlle  21634  thloc  21636  dsmmval2  21673  psrmulr  21879  mplmonmul  21971  mplcoe3  21973  opsrbaslem  21984  opsrtoslem2  21991  psr1val  22098  ply1basfvi  22153  ply1plusgfvi  22154  psr1sca2  22163  evl1fval1lem  22245  mattpos1  22371  mdettpos  22526  smadiadetglem1  22586  tgdif0  22907  indislem  22915  restco  23079  txtopon  23506  txindislem  23548  qtopres  23613  hmphindis  23712  ptuncnv  23722  snclseqg  24031  tsmssplit  24067  ussval  24174  tuslem  24181  setsmsbas  24390  tngds  24563  tngtset  24564  pcoass  24951  cphsqrtcl2  25113  rrxcph  25319  ovolunlem1a  25424  ioorinv  25504  itg11  25619  itg1mulc  25632  itg2cnlem1  25689  iblss2  25734  ibladdlem  25748  itgfsum  25755  iblabslem  25756  iblabs  25757  ditgneg  25785  deg1fvi  26017  dgrco  26208  logfac  26537  cxpexp  26604  cxpmul2  26625  cxpsqrt  26639  cxpsqrtth  26666  dvcxp1  26676  dvcxp2  26677  ang180lem1  26746  mcubic  26784  quart1  26793  reasinsin  26833  atanlogaddlem  26850  atantayl2  26875  log2tlbnd  26882  basellem2  27019  basellem3  27020  basellem5  27022  basellem8  27025  fsumdvdsmul  27132  dchrmullid  27190  bcp1ctr  27217  lgsneg  27259  lgsneg1  27260  lgsdir2  27268  lgsdir  27270  lgsdi  27272  lgsquad2lem2  27323  pntleml  27549  lrold  27842  abssnid  28181  om2noseqfo  28228  n0seo  28344  pw2cutp1  28381  zs12bday  28394  motgrp  28521  lmiisolem  28774  egrsubgr  29255  iswwlksnon  29831  iswspthsnon  29834  bafval  30584  ipidsq  30690  ipasslem1  30811  pjclem2  32176  cvmdi  32304  imadifxp  32581  2ndimaxp  32628  suppun2  32665  iundisjcnt  32780  indval2  32835  dpfrac1  32872  gsumpart  33037  cycpmco2rn  33094  cyc3genpmlem  33120  fracbas  33271  resvsca  33297  rspectset  33879  bayesth  34452  ofcccat  34556  plymulx  34561  subfacp1lem6  35229  satfdm  35413  mvtval  35544  mexval  35546  mexval2  35547  mdvval  35548  mrsubfval  35552  mrsubvrs  35566  msubfval  35568  elmsubrn  35572  mvhfval  35577  mpstval  35579  msrfval  35581  mstaval  35588  mthmval  35619  bccolsum  35783  dfrdg2  35837  dfrdg3  35838  dfrdg4  35993  ordtoplem  36477  ordcmp  36489  curunc  37650  matunitlindflem2  37665  poimirlem6  37674  poimirlem7  37675  poimirlem11  37679  poimirlem12  37680  poimirlem13  37681  poimirlem14  37682  poimirlem16  37684  poimirlem19  37687  poimirlem21  37689  poimirlem22  37690  poimirlem27  37695  poimirlem31  37699  poimirlem32  37700  itg2addnclem2  37720  ibladdnclem  37724  iblabsnclem  37731  iblabsnc  37732  iblmulc2nc  37733  ftc1anclem8  37748  pmodN  39897  tgrpgrplem  40796  tendoplass  40830  tendoicl  40843  erngdvlem3  41037  dvhvaddass  41144  dib0  41211  dib1dim2  41215  diclspsn  41241  cdlemn8  41251  dihopelvalcpre  41295  djhcom  41452  evlsbagval  42607  kelac2  43106  mendbas  43221  mendring  43229  iscard4  43574  relexp01min  43754  relexpaddss  43759  iotain  44458  addrcom  44515  rnsnf  45229  itgsinexplem1  46000  volioc  46018  dirkertrigeqlem1  46144  fourierdlem104  46256  sqwvfoura  46274  sqwvfourb  46275  fzopredsuc  47362  fppr2odd  47770  dfnbgr5  47890  gpgprismgr4cycllem10  48143  rngccatidALTV  48311  ringccatidALTV  48345  0dig2pr01  48650  nn0sumshdiglemB  48660  imaidfu2  49151  oppczeroo  49277  dfswapf2  49301  oppc1stf  49328  oppc2ndf  49329  prcof1  49428  setc1onsubc  49642  termolmd  49710