Theorem 3eqtr3a 2821

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 2809	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2799	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 2734

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

This theorem is used by:  uneqin  4238  coi2  6264  foima  6798  f1imacnv  6838  fvsnun1  7184  fnsnsplit  7186  phplem2  9203  php3  9207  rankopb  9838  fin4en1  10315  fpwwe2  10656  winacard  10705  mul02lem1  11414  cnegex2  11420  crreczi  14296  hashinf  14403  hashcard  14423  cshw0  14869  cshwn  14872  sqrtneglem  15357  rlimresb  15656  bpoly3  16150  bpoly4  16151  sinhval  16248  coshval  16249  absefib  16292  efieq1re  16293  sadcaddlem  16553  sadaddlem  16562  qus0subgbas  19332  psgnsn  19653  odngen  19710  frlmup3  22019  mat0op  22647  restopnb  23406  cnmpt2t  23905  clmnegneg  25338  ncvspi  25390  volsup2  25839  plypf1  26445  pige3ALT  26765  sineq0  26769  eflog  26821  logef  26826  cxpsqrt  26948  dvcncxp1  26988  cubic2  27093  quart1  27101  asinsinlem  27136  asinsin  27137  2efiatan  27163  pclogsum  27459  lgsneg  27565  bdayfinbndlem1  28740  vc0  31063  vcm  31065  nvpi  31156  honegneg  32295  opsqrlem6  32634  sto1i  32725  mdexchi  32824  fmptunsnop  33180  preiman0  33190  elrspunidl  33864  cnre2csqlem  34428  itgexpif  35122  subfacp1lem1  35766  rankaltopb  36567  poimirlem23  38400  dvtan  38427  dvasin  38461  heiborlem6  38574  trlcoat  41604  cdlemk54  41839  readvcot  43247  resubid  43292  sn-mul02  43348  iocunico  44060  relintab  44431  rfovcnvf1od  44852  ntrneifv3  44930  ntrneifv4  44933  clsneifv3  44958  clsneifv4  44959  neicvgfv  44969  snunioo1  46350  dvsinexp  46747  dvnprodlem1  46782  itgsubsticclem  46811  stirlinglem1  46910  fourierdlem80  47022  fourierdlem111  47053  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  saliinclf  47162  smfco  47638  2oppf  50066  aacllem  50780