Theorem 3eqtr3a 2880

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 2868	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2858	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 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  uneqin  4254  coi2  6115  foima  6594  f1imacnv  6630  fvsnun1  6943  fnsnsplit  6945  phplem4  8698  php3  8702  rankopb  9280  fin4en1  9730  fpwwe2  10064  winacard  10113  mul02lem1  10815  cnegex2  10821  crreczi  13588  hashinf  13694  hashcard  13715  cshw0  14155  cshwn  14158  sqrtneglem  14625  rlimresb  14921  bpoly3  15411  bpoly4  15412  sinhval  15506  coshval  15507  absefib  15550  efieq1re  15551  sadcaddlem  15805  sadaddlem  15814  psgnsn  18647  odngen  18701  frlmup3  20943  mat0op  21027  restopnb  21782  cnmpt2t  22280  clmnegneg  23707  ncvspi  23759  volsup2  24205  plypf1  24801  pige3ALT  25104  sineq0  25108  eflog  25159  logef  25164  cxpsqrt  25285  dvcncxp1  25323  cubic2  25425  quart1  25433  asinsinlem  25468  asinsin  25469  2efiatan  25495  pclogsum  25790  lgsneg  25896  vc0  28350  vcm  28352  nvpi  28443  honegneg  29582  opsqrlem6  29921  sto1i  30012  mdexchi  30111  cnre2csqlem  31153  itgexpif  31877  subfacp1lem1  32426  rankaltopb  33440  poimirlem23  34914  dvtan  34941  dvasin  34977  heiborlem6  35093  trlcoat  37858  cdlemk54  38093  resubid  39236  iocunico  39815  relintab  39941  rfovcnvf1od  40348  ntrneifv3  40430  ntrneifv4  40433  clsneifv3  40458  clsneifv4  40459  neicvgfv  40469  snunioo1  41786  dvsinexp  42193  itgsubsticclem  42258  stirlinglem1  42358  fourierdlem80  42470  fourierdlem111  42501  sqwvfoura  42512  sqwvfourb  42513  fouriersw  42515  aacllem  44901