Theorem 3eqtr3a 2822

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

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  uneqin  4242  coi2  6265  foima  6797  f1imacnv  6837  fvsnun1  7180  fnsnsplit  7182  phplem2  9185  php3  9189  rankopb  9820  fin4en1  10288  fpwwe2  10623  winacard  10672  mul02lem1  11381  cnegex2  11387  crreczi  14260  hashinf  14367  hashcard  14387  cshw0  14827  cshwn  14830  sqrtneglem  15313  rlimresb  15612  bpoly3  16107  bpoly4  16108  sinhval  16205  coshval  16206  absefib  16249  efieq1re  16250  sadcaddlem  16510  sadaddlem  16519  qus0subgbas  19264  psgnsn  19585  odngen  19642  frlmup3  21950  mat0op  22576  restopnb  23332  cnmpt2t  23830  clmnegneg  25263  ncvspi  25315  volsup2  25764  plypf1  26369  pige3ALT  26685  sineq0  26689  eflog  26741  logef  26746  cxpsqrt  26868  dvcncxp1  26908  cubic2  27013  quart1  27021  asinsinlem  27056  asinsin  27057  2efiatan  27083  pclogsum  27379  lgsneg  27485  bdayfinbndlem1  28660  vc0  30926  vcm  30928  nvpi  31019  honegneg  32158  opsqrlem6  32497  sto1i  32588  mdexchi  32687  fmptunsnop  33045  preiman0  33055  elrspunidl  33736  cnre2csqlem  34300  itgexpif  34993  subfacp1lem1  35671  rankaltopb  36471  poimirlem23  38294  dvtan  38321  dvasin  38355  heiborlem6  38467  trlcoat  41497  cdlemk54  41732  readvcot  43125  resubid  43170  sn-mul02  43226  iocunico  43938  relintab  44309  rfovcnvf1od  44730  ntrneifv3  44808  ntrneifv4  44811  clsneifv3  44836  clsneifv4  44837  neicvgfv  44847  snunioo1  46228  dvsinexp  46625  dvnprodlem1  46660  itgsubsticclem  46689  stirlinglem1  46788  fourierdlem80  46900  fourierdlem111  46931  sqwvfoura  46942  sqwvfourb  46943  fouriersw  46945  saliinclf  47040  smfco  47516  2oppf  49910  aacllem  50621