Theorem 3eqtr3a 2839

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	syl5eq 2827	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2817	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2772

This theorem is referenced by:  uneqin  4143  coi2  5955  foima  6424  f1imacnv  6460  fvsnun1  6769  fvsnun2OLD  6772  fnsnsplit  6773  phplem4  8495  php3  8499  rankopb  9075  fin4en1  9529  fpwwe2  9863  winacard  9912  mul02lem1  10616  cnegex2  10622  crreczi  13404  hashinf  13510  hashcard  13531  cshw0  14018  cshwn  14021  sqrtneglem  14487  rlimresb  14783  bpoly3  15272  bpoly4  15273  sinhval  15367  coshval  15368  absefib  15411  efieq1re  15412  sadcaddlem  15666  sadaddlem  15675  psgnsn  18410  odngen  18463  frlmup3  20646  mat0op  20732  restopnb  21487  cnmpt2t  21985  clmnegneg  23411  ncvspi  23463  volsup2  23909  plypf1  24505  pige3ALT  24808  sineq0  24812  eflog  24861  logef  24866  cxpsqrt  24987  dvcncxp1  25025  cubic2  25127  quart1  25135  asinsinlem  25170  asinsin  25171  2efiatan  25197  pclogsum  25493  lgsneg  25599  vc0  28128  vcm  28130  nvpi  28221  honegneg  29364  opsqrlem6  29703  sto1i  29794  mdexchi  29893  cnre2csqlem  30794  itgexpif  31522  subfacp1lem1  32008  rankaltopb  32958  poimirlem23  34353  dvtan  34380  dvasin  34416  heiborlem6  34533  trlcoat  37301  cdlemk54  37536  iocunico  39210  relintab  39302  rfovcnvf1od  39710  ntrneifv3  39792  ntrneifv4  39795  clsneifv3  39820  clsneifv4  39821  neicvgfv  39831  snunioo1  41217  dvsinexp  41623  itgsubsticclem  41688  stirlinglem1  41788  fourierdlem80  41900  fourierdlem111  41931  sqwvfoura  41942  sqwvfourb  41943  fouriersw  41945  aacllem  44267