Theorem 3eqtr3a 2795

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  uneqin  4278  coi2  6262  foima  6810  f1imacnv  6849  fvsnun1  7182  fnsnsplit  7184  phplem2  9211  php3  9215  phplem4OLD  9223  php3OLD  9227  rankopb  9850  fin4en1  10307  fpwwe2  10641  winacard  10690  mul02lem1  11395  cnegex2  11401  crreczi  14196  hashinf  14300  hashcard  14320  cshw0  14749  cshwn  14752  sqrtneglem  15218  rlimresb  15514  bpoly3  16007  bpoly4  16008  sinhval  16102  coshval  16103  absefib  16146  efieq1re  16147  sadcaddlem  16403  sadaddlem  16412  qus0subgbas  19114  psgnsn  19430  odngen  19487  frlmup3  21575  mat0op  22142  restopnb  22900  cnmpt2t  23398  clmnegneg  24852  ncvspi  24905  volsup2  25355  plypf1  25962  pige3ALT  26266  sineq0  26270  eflog  26322  logef  26327  cxpsqrt  26448  dvcncxp1  26488  cubic2  26590  quart1  26598  asinsinlem  26633  asinsin  26634  2efiatan  26660  pclogsum  26955  lgsneg  27061  vc0  30095  vcm  30097  nvpi  30188  honegneg  31327  opsqrlem6  31666  sto1i  31757  mdexchi  31856  preiman0  32199  elrspunidl  32821  cnre2csqlem  33189  itgexpif  33917  subfacp1lem1  34469  rankaltopb  35256  poimirlem23  36815  dvtan  36842  dvasin  36876  heiborlem6  36988  trlcoat  39898  cdlemk54  40133  resubid  41584  sn-mul02  41616  iocunico  42263  relintab  42637  rfovcnvf1od  43058  ntrneifv3  43136  ntrneifv4  43139  clsneifv3  43164  clsneifv4  43165  neicvgfv  43175  snunioo1  44524  dvsinexp  44926  itgsubsticclem  44990  stirlinglem1  45089  fourierdlem80  45201  fourierdlem111  45232  sqwvfoura  45243  sqwvfourb  45244  fouriersw  45246  saliinclf  45341  smfco  45817  aacllem  47936