Theorem 3eqtr3a 2820

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  uneqin  4235  coi2  6264  foima  6799  f1imacnv  6839  fvsnun1  7185  fnsnsplit  7187  phplem2  9213  php3  9217  rankopb  9859  fin4en1  10380  fpwwe2  10721  winacard  10770  mul02lem1  11479  cnegex2  11485  crreczi  14365  hashinf  14472  hashcard  14492  cshw0  14938  cshwn  14941  sqrtneglem  15426  rlimresb  15725  bpoly3  16217  bpoly4  16218  sinhval  16315  coshval  16316  absefib  16359  efieq1re  16360  sadcaddlem  16620  sadaddlem  16629  qus0subgbas  19406  psgnsn  19727  odngen  19784  frlmup3  22099  mat0op  22727  restopnb  23486  cnmpt2t  23985  clmnegneg  25418  ncvspi  25470  volsup2  25919  plypf1  26524  pige3ALT  26841  sineq0  26845  eflog  26897  logef  26902  cxpsqrt  27024  dvcncxp1  27064  cubic2  27169  quart1  27177  asinsinlem  27212  asinsin  27213  2efiatan  27239  pclogsum  27535  lgsneg  27641  bdayfinbndlem1  28846  vc0  31169  vcm  31171  nvpi  31262  honegneg  32401  opsqrlem6  32740  sto1i  32831  mdexchi  32930  fmptunsnop  33286  preiman0  33296  elrspunidl  33971  cnre2csqlem  34535  itgexpif  35228  subfacp1lem1  35923  rankaltopb  36724  poimirlem23  38541  dvtan  38568  dvasin  38602  heiborlem6  38730  trlcoat  41760  cdlemk54  41995  readvcot  43395  resubid  43440  sn-mul02  43496  iocunico  44197  relintab  44568  rfovcnvf1od  44989  ntrneifv3  45067  ntrneifv4  45070  clsneifv3  45095  clsneifv4  45096  neicvgfv  45106  snunioo1  46493  dvsinexp  46890  dvnprodlem1  46925  itgsubsticclem  46954  stirlinglem1  47053  fourierdlem80  47165  fourierdlem111  47196  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  saliinclf  47305  smfco  47781  2oppf  50209  aacllem  50908