Theorem 3eqtr3a 2789

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 2777	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2767	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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  uneqin  4277  coi2  6269  foima  6815  f1imacnv  6854  fvsnun1  7191  fnsnsplit  7193  phplem2  9233  php3  9237  phplem4OLD  9245  php3OLD  9249  rankopb  9877  fin4en1  10334  fpwwe2  10668  winacard  10717  mul02lem1  11422  cnegex2  11428  crreczi  14226  hashinf  14330  hashcard  14350  cshw0  14780  cshwn  14783  sqrtneglem  15249  rlimresb  15545  bpoly3  16038  bpoly4  16039  sinhval  16134  coshval  16135  absefib  16178  efieq1re  16179  sadcaddlem  16435  sadaddlem  16444  qus0subgbas  19161  psgnsn  19487  odngen  19544  frlmup3  21751  mat0op  22365  restopnb  23123  cnmpt2t  23621  clmnegneg  25075  ncvspi  25128  volsup2  25578  plypf1  26191  pige3ALT  26499  sineq0  26503  eflog  26555  logef  26560  cxpsqrt  26682  dvcncxp1  26722  cubic2  26825  quart1  26833  asinsinlem  26868  asinsin  26869  2efiatan  26895  pclogsum  27193  lgsneg  27299  vc0  30456  vcm  30458  nvpi  30549  honegneg  31688  opsqrlem6  32027  sto1i  32118  mdexchi  32217  preiman0  32571  elrspunidl  33240  cnre2csqlem  33639  itgexpif  34366  subfacp1lem1  34917  rankaltopb  35703  poimirlem23  37244  dvtan  37271  dvasin  37305  heiborlem6  37417  trlcoat  40323  cdlemk54  40558  resubid  42095  sn-mul02  42127  iocunico  42778  relintab  43152  rfovcnvf1od  43573  ntrneifv3  43651  ntrneifv4  43654  clsneifv3  43679  clsneifv4  43680  neicvgfv  43690  snunioo1  45032  dvsinexp  45434  itgsubsticclem  45498  stirlinglem1  45597  fourierdlem80  45709  fourierdlem111  45740  sqwvfoura  45751  sqwvfourb  45752  fouriersw  45754  saliinclf  45849  smfco  46325  aacllem  48417