Theorem 3eqtr3a 2802

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  uneqin  4213  coi2  6161  foima  6686  f1imacnv  6725  fvsnun1  7047  fnsnsplit  7049  phplem2  8979  php3  8983  phplem4OLD  8991  php3OLD  8995  rankopb  9598  fin4en1  10053  fpwwe2  10387  winacard  10436  mul02lem1  11139  cnegex2  11145  crreczi  13931  hashinf  14037  hashcard  14058  cshw0  14495  cshwn  14498  sqrtneglem  14966  rlimresb  15262  bpoly3  15756  bpoly4  15757  sinhval  15851  coshval  15852  absefib  15895  efieq1re  15896  sadcaddlem  16152  sadaddlem  16161  psgnsn  19116  odngen  19170  frlmup3  20995  mat0op  21556  restopnb  22314  cnmpt2t  22812  clmnegneg  24255  ncvspi  24308  volsup2  24757  plypf1  25361  pige3ALT  25664  sineq0  25668  eflog  25720  logef  25725  cxpsqrt  25846  dvcncxp1  25884  cubic2  25986  quart1  25994  asinsinlem  26029  asinsin  26030  2efiatan  26056  pclogsum  26351  lgsneg  26457  vc0  28922  vcm  28924  nvpi  29015  honegneg  30154  opsqrlem6  30493  sto1i  30584  mdexchi  30683  preiman0  31028  elrspunidl  31592  cnre2csqlem  31846  itgexpif  32572  subfacp1lem1  33127  rankaltopb  34267  poimirlem23  35786  dvtan  35813  dvasin  35847  heiborlem6  35960  trlcoat  38723  cdlemk54  38958  resubid  40377  sn-mul02  40408  iocunico  41028  relintab  41150  rfovcnvf1od  41571  ntrneifv3  41651  ntrneifv4  41654  clsneifv3  41679  clsneifv4  41680  neicvgfv  41690  snunioo1  43009  dvsinexp  43411  itgsubsticclem  43475  stirlinglem1  43574  fourierdlem80  43686  fourierdlem111  43717  sqwvfoura  43728  sqwvfourb  43729  fouriersw  43731  smfco  44292  aacllem  46461