Theorem 3eqtr3a 2797

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

Syntax hints:   → wi 4   = wceq 1542

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  uneqin  4279  coi2  6263  foima  6811  f1imacnv  6850  fvsnun1  7180  fnsnsplit  7182  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  rankopb  9847  fin4en1  10304  fpwwe2  10638  winacard  10687  mul02lem1  11390  cnegex2  11396  crreczi  14191  hashinf  14295  hashcard  14315  cshw0  14744  cshwn  14747  sqrtneglem  15213  rlimresb  15509  bpoly3  16002  bpoly4  16003  sinhval  16097  coshval  16098  absefib  16141  efieq1re  16142  sadcaddlem  16398  sadaddlem  16407  qus0subgbas  19075  psgnsn  19388  odngen  19445  frlmup3  21355  mat0op  21921  restopnb  22679  cnmpt2t  23177  clmnegneg  24620  ncvspi  24673  volsup2  25122  plypf1  25726  pige3ALT  26029  sineq0  26033  eflog  26085  logef  26090  cxpsqrt  26211  dvcncxp1  26251  cubic2  26353  quart1  26361  asinsinlem  26396  asinsin  26397  2efiatan  26423  pclogsum  26718  lgsneg  26824  vc0  29858  vcm  29860  nvpi  29951  honegneg  31090  opsqrlem6  31429  sto1i  31520  mdexchi  31619  preiman0  31962  elrspunidl  32577  cnre2csqlem  32921  itgexpif  33649  subfacp1lem1  34201  rankaltopb  34982  poimirlem23  36559  dvtan  36586  dvasin  36620  heiborlem6  36732  trlcoat  39642  cdlemk54  39877  resubid  41329  sn-mul02  41361  iocunico  42008  relintab  42382  rfovcnvf1od  42803  ntrneifv3  42881  ntrneifv4  42884  clsneifv3  42909  clsneifv4  42910  neicvgfv  42920  snunioo1  44273  dvsinexp  44675  itgsubsticclem  44739  stirlinglem1  44838  fourierdlem80  44950  fourierdlem111  44981  sqwvfoura  44992  sqwvfourb  44993  fouriersw  44995  saliinclf  45090  smfco  45566  aacllem  47896