Theorem 3eqtr4a 2822

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  rabsnif  4684  uniintsn  4945  iinvdif  5040  iununi  5059  csbcnv  5864  dmxpid  5912  rnxpid  6165  csbrn  6203  dmsnsnsn  6220  opswap  6229  xpcoid  6292  predres  6341  unizlim  6486  fvco4i  6985  fndmdifcom  7040  fmptsng  7171  fmptsnd  7172  csbov  7463  ordunisuc  7841  offres  7993  1stval2  8016  2ndval2  8017  cnvf1olem  8119  fparlem3  8123  fparlem4  8124  frrlem12  8308  seqomlem1  8453  ecovcom  8837  ecovass  8838  ecovdi  8839  resixpfo  8957  mapunen  9158  cardidm  10033  cardiun  10056  alephcard  10142  cardalephex  10162  cardcf  10322  cfidm  10346  alephsing  10347  itunisuc  10490  itunitc  10492  ituniiun  10493  alephadd  10655  alephreg  10660  pwcfsdom  10661  addcompq  11028  addcomnq  11029  mulcompq  11030  mulcomnq  11031  addassnq  11036  mulassnq  11037  addrid  11483  indval2  12318  zeo  12778  xnegneg  13337  xaddcom  13363  xaddrid  13364  xnegdi  13371  xmulrid  13402  xadddilem  13417  ixxin  13486  fzsuc2  13709  expneg  14205  sq01  14362  facp1  14415  bcpasc  14458  hashfzp1  14569  resunimafz0  14583  hashf1lem1  14593  hashf1  14595  ccat1st1st  14769  swrdccatin1  14867  swrdccat3blem  14881  repswsymballbi  14924  cshwmodn  14939  cshwlen  14943  repswcshw  14956  trclun  15160  relexpcnv  15181  relexpaddd  15200  absexp  15464  sqreulem  15520  fsumf1o  15882  fsumadd  15899  fsumrev2  15941  fsumparts  15966  fsumrelem  15967  fprodf1o  16106  fprodmul  16120  fproddiv  16121  fprodfac  16133  fallfacfwd  16195  efexp  16262  tanval2  16294  sadeq  16635  smumullem  16655  smumul  16656  gcdcom  16678  gcd0id  16684  gcdass  16713  nn0expgcd  16731  lcmcom  16761  lcmneg  16771  lcmass  16782  nn0gcdsq  16921  dfphi2  16944  pcneg  17045  setscom  17351  strfvi  17361  fveqprc  17362  oveqprc  17363  ressbas  17407  ressinbas  17416  ressress  17418  firest  17596  topnval  17598  xpsfeq  17728  xpsaddlem  17738  xpsvsca  17742  oppchomfval  17881  rescbas  17997  rescco  18000  cofuass  18057  fucbas  18131  fuchom  18132  setccatid  18252  estrccatid  18299  xpcbas  18345  oduleval  18456  odulub  18572  oduglb  18574  ipotset  18700  mgmn0plusgplusf  18821  efmndbas  19060  efmndbasabf  19061  symggrplem  19073  smndex1mndlem  19101  pwmnd  19136  grpinvfvi  19186  cntrval  19526  cntzval  19528  oppgplusfval  19555  snsymgefmndeq  19602  symgvalstruct  19604  pmtrprfval  19694  m1expaddsub  19705  sylow1lem2  19806  sylow3lem1  19834  oppglsm  19849  gsumzsplit  20134  gsum2dlem2  20178  gsumcom2  20182  dprd2dlem2  20249  dprd2da  20251  dmdprdsplit2lem  20254  mgpplusg  20357  mgpress  20363  ringidval  20402  opprmulfval  20562  abvtrivd  21082  sralem  21444  srasca  21448  sravsca  21449  sraip  21450  rlmval  21459  zlmsca  21819  zlmvsca  21820  psgninv  21881  ocvval  21966  thlbas  21995  thlle  21996  thloc  21998  dsmmval2  22035  psrmulr  22243  mplmonmul  22338  mplcoe3  22340  opsrbaslem  22351  opsrtoslem2  22358  psr1val  22497  ply1basfvi  22551  ply1plusgfvi  22552  psr1sca2  22561  evl1fval1lem  22641  mattpos1  22764  mdettpos  22919  smadiadetglem1  22979  matunitlindflem2  22988  tgdif0  23303  indislem  23311  restco  23475  txtopon  23903  txindislem  23945  qtopres  24010  hmphindis  24109  ptuncnv  24119  snclseqg  24428  tsmssplit  24464  ussval  24571  tuslem  24578  setsmsbas  24787  tngds  24960  tngtset  24961  pcoass  25338  cphsqrtcl2  25500  rrxcph  25706  ovolunlem1a  25810  ioorinv  25890  itg11  26005  itg1mulc  26018  itg2cnlem1  26075  iblss2  26119  ibladdlem  26133  itgfsum  26140  iblabslem  26141  iblabs  26142  ditgneg  26170  deg1fvi  26396  dgrco  26587  plymulidp  26596  logfac  26922  cxpexp  26989  cxpmul2  27010  cxpsqrt  27024  cxpsqrtth  27051  dvcxp1  27061  dvcxp2  27062  ang180lem1  27130  mcubic  27168  quart1  27177  reasinsin  27217  atanlogaddlem  27234  atantayl2  27259  log2tlbnd  27266  basellem2  27402  basellem3  27403  basellem5  27405  basellem8  27408  fsumdvdsmul  27515  dchrmullid  27572  bcp1ctr  27599  lgsneg  27641  lgsneg1  27642  lgsdir2  27650  lgsdir  27652  lgsdi  27654  lgsquad2lem2  27705  pntleml  27931  lrold  28276  abssnid  28622  om2noseqfo  28677  n0seo  28800  pw2cutp1  28840  motgrp  28999  lmiisolem  29294  egrsubgr  29851  iswwlksnon  30435  iswspthsnon  30438  bafval  31199  ipidsq  31305  ipasslem1  31426  pjclem2  32791  cvmdi  32919  imadifxp  33188  2ndimaxp  33233  suppun2  33270  iundisjcnt  33383  dpfrac1  33451  gsumpart  33617  suppgsumssiun  33626  cycpmco2rn  33679  cyc3genpmlem  33705  fracbas  33860  resvsca  33886  psrgsum  34173  psrmonmul  34175  psrmonprod  34177  rspectset  34491  bayesth  35064  ofcccat  35168  subfacp1lem6  35929  satfdm  36113  mvtval  36244  mexval  36246  mexval2  36247  mdvval  36248  mrsubfval  36252  mrsubvrs  36266  msubfval  36268  elmsubrn  36272  mvhfval  36277  mpstval  36279  msrfval  36281  mstaval  36288  mthmval  36319  bccolsum  36483  dfrdg2  36537  dfrdg3  36538  dfrdg4  36695  ordtoplem  37203  ordcmp  37215  curunc  38505  poimirlem6  38524  poimirlem7  38525  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem16  38534  poimirlem19  38537  poimirlem21  38539  poimirlem22  38540  poimirlem27  38545  poimirlem31  38549  poimirlem32  38550  itg2addnclem2  38570  ibladdnclem  38574  iblabsnclem  38581  iblabsnc  38582  iblmulc2nc  38583  ftc1anclem8  38598  pmodN  40887  tgrpgrplem  41786  tendoplass  41820  tendoicl  41833  erngdvlem3  42027  dvhvaddass  42134  dib0  42201  dib1dim2  42205  diclspsn  42231  cdlemn8  42241  dihopelvalcpre  42285  djhcom  42442  evlsbagval  43594  kelac2  44051  mendbas  44166  mendring  44174  iscard4  44518  relexp01min  44698  relexpaddss  44703  iotain  45386  addrcom  45442  rnsnf  46168  limsupvaluz  46687  itgsinexplem1  46933  volioc  46951  dirkertrigeqlem1  47077  fourierdlem104  47189  sqwvfoura  47207  sqwvfourb  47208  hoicvr  47527  fzopredsuc  48363  ppivalnn  48686  fppr2odd  48798  dfnbgr5  48918  gpgprismgr4cycllem10  49171  rngccatidALTV  49338  ringccatidALTV  49372  0dig2pr01  49691  nn0sumshdiglemB  49701  imaidfu2  50188  oppczeroo  50314  dfswapf2  50338  oppc1stf  50365  oppc2ndf  50366  prcof1  50465  setc1onsubc  50679  termolmd  50747