Theorem 3eqtr3a 2819

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 2807	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2797	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 2732

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

This theorem is used by:  uneqin  4235  coi2  6260  foima  6794  f1imacnv  6834  fvsnun1  7180  fnsnsplit  7182  phplem2  9199  php3  9203  rankopb  9834  fin4en1  10311  fpwwe2  10652  winacard  10701  mul02lem1  11410  cnegex2  11416  crreczi  14292  hashinf  14399  hashcard  14419  cshw0  14865  cshwn  14868  sqrtneglem  15353  rlimresb  15652  bpoly3  16144  bpoly4  16145  sinhval  16242  coshval  16243  absefib  16286  efieq1re  16287  sadcaddlem  16547  sadaddlem  16556  qus0subgbas  19326  psgnsn  19647  odngen  19704  frlmup3  22013  mat0op  22641  restopnb  23400  cnmpt2t  23899  clmnegneg  25332  ncvspi  25384  volsup2  25833  plypf1  26438  pige3ALT  26757  sineq0  26761  eflog  26813  logef  26818  cxpsqrt  26940  dvcncxp1  26980  cubic2  27085  quart1  27093  asinsinlem  27128  asinsin  27129  2efiatan  27155  pclogsum  27451  lgsneg  27557  bdayfinbndlem1  28732  vc0  31055  vcm  31057  nvpi  31148  honegneg  32287  opsqrlem6  32626  sto1i  32717  mdexchi  32816  fmptunsnop  33172  preiman0  33182  elrspunidl  33856  cnre2csqlem  34420  itgexpif  35114  subfacp1lem1  35758  rankaltopb  36559  poimirlem23  38392  dvtan  38419  dvasin  38453  heiborlem6  38566  trlcoat  41596  cdlemk54  41831  readvcot  43239  resubid  43284  sn-mul02  43340  iocunico  44052  relintab  44423  rfovcnvf1od  44844  ntrneifv3  44922  ntrneifv4  44925  clsneifv3  44950  clsneifv4  44951  neicvgfv  44961  snunioo1  46342  dvsinexp  46739  dvnprodlem1  46774  itgsubsticclem  46803  stirlinglem1  46902  fourierdlem80  47014  fourierdlem111  47045  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  saliinclf  47154  smfco  47630  2oppf  50058  aacllem  50772