Theorem 3eqtr3a 2828

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  uneqin  4250  coi2  6263  foima  6795  f1imacnv  6835  fvsnun1  7178  fnsnsplit  7180  phplem2  9185  php3  9189  rankopb  9820  fin4en1  10289  fpwwe2  10624  winacard  10673  mul02lem1  11382  cnegex2  11388  crreczi  14260  hashinf  14367  hashcard  14387  cshw0  14827  cshwn  14830  sqrtneglem  15313  rlimresb  15612  bpoly3  16108  bpoly4  16109  sinhval  16206  coshval  16207  absefib  16250  efieq1re  16251  sadcaddlem  16511  sadaddlem  16520  qus0subgbas  19265  psgnsn  19586  odngen  19643  frlmup3  21915  mat0op  22541  restopnb  23297  cnmpt2t  23795  clmnegneg  25228  ncvspi  25280  volsup2  25729  plypf1  26334  pige3ALT  26647  sineq0  26651  eflog  26703  logef  26708  cxpsqrt  26830  dvcncxp1  26870  cubic2  26975  quart1  26983  asinsinlem  27018  asinsin  27019  2efiatan  27045  pclogsum  27341  lgsneg  27447  bdayfinbndlem1  28622  vc0  30863  vcm  30865  nvpi  30956  honegneg  32095  opsqrlem6  32434  sto1i  32525  mdexchi  32624  fmptunsnop  32982  preiman0  32992  elrspunidl  33676  cnre2csqlem  34241  itgexpif  34934  subfacp1lem1  35566  rankaltopb  36366  poimirlem23  38177  dvtan  38204  dvasin  38238  heiborlem6  38350  trlcoat  41382  cdlemk54  41617  readvcot  43010  resubid  43055  sn-mul02  43111  iocunico  43825  relintab  44196  rfovcnvf1od  44617  ntrneifv3  44695  ntrneifv4  44698  clsneifv3  44723  clsneifv4  44724  neicvgfv  44734  snunioo1  46115  dvsinexp  46512  dvnprodlem1  46547  itgsubsticclem  46576  stirlinglem1  46675  fourierdlem80  46787  fourierdlem111  46818  sqwvfoura  46829  sqwvfourb  46830  fouriersw  46832  saliinclf  46927  smfco  47403  2oppf  49790  aacllem  50470