Theorem 3eqtr3a 2796

Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)

Hypotheses

Ref	Expression
3eqtr3a.1	⊢ 𝐴 = 𝐵
3eqtr3a.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3a.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

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

Proof of Theorem 3eqtr3a

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3eqtr3a.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3a.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	eqtrid 2784	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2774	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  uneqin  4230  coi2  6222  foima  6751  f1imacnv  6790  fvsnun1  7130  fnsnsplit  7132  phplem2  9132  php3  9136  rankopb  9767  fin4en1  10222  fpwwe2  10557  winacard  10606  mul02lem1  11313  cnegex2  11319  crreczi  14181  hashinf  14288  hashcard  14308  cshw0  14747  cshwn  14750  sqrtneglem  15219  rlimresb  15518  bpoly3  16014  bpoly4  16015  sinhval  16112  coshval  16113  absefib  16156  efieq1re  16157  sadcaddlem  16417  sadaddlem  16426  qus0subgbas  19164  psgnsn  19486  odngen  19543  frlmup3  21790  mat0op  22394  restopnb  23150  cnmpt2t  23648  clmnegneg  25081  ncvspi  25133  volsup2  25582  plypf1  26187  pige3ALT  26497  sineq0  26501  eflog  26553  logef  26558  cxpsqrt  26680  dvcncxp1  26720  cubic2  26825  quart1  26833  asinsinlem  26868  asinsin  26869  2efiatan  26895  pclogsum  27192  lgsneg  27298  bdayfinbndlem1  28473  vc0  30660  vcm  30662  nvpi  30753  honegneg  31892  opsqrlem6  32231  sto1i  32322  mdexchi  32421  fmptunsnop  32788  preiman0  32798  elrspunidl  33503  cnre2csqlem  34070  itgexpif  34766  subfacp1lem1  35377  rankaltopb  36177  poimirlem23  37978  dvtan  38005  dvasin  38039  heiborlem6  38151  trlcoat  41183  cdlemk54  41418  readvcot  42810  resubid  42855  sn-mul02  42911  iocunico  43657  relintab  44028  rfovcnvf1od  44449  ntrneifv3  44527  ntrneifv4  44530  clsneifv3  44555  clsneifv4  44556  neicvgfv  44566  snunioo1  45960  dvsinexp  46357  dvnprodlem1  46392  itgsubsticclem  46421  stirlinglem1  46520  fourierdlem80  46632  fourierdlem111  46663  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  saliinclf  46772  smfco  47248  2oppf  49619  aacllem  50288