Theorem 3eqtr3a 2798

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  uneqin  4217  coi2  6215  foima  6744  f1imacnv  6783  fvsnun1  7126  fnsnsplit  7128  phplem2  9129  php3  9133  rankopb  9767  fin4en1  10222  fpwwe2  10557  winacard  10606  mul02lem1  11313  cnegex2  11319  crreczi  14181  hashinf  14288  hashcard  14308  cshw0  14747  cshwn  14750  sqrtneglem  15219  rlimresb  15518  bpoly3  16014  bpoly4  16015  sinhval  16112  coshval  16113  absefib  16156  efieq1re  16157  sadcaddlem  16417  sadaddlem  16426  qus0subgbas  19164  psgnsn  19486  odngen  19543  frlmup3  21775  mat0op  22402  restopnb  23158  cnmpt2t  23656  clmnegneg  25089  ncvspi  25141  volsup2  25590  plypf1  26195  pige3ALT  26502  sineq0  26506  eflog  26558  logef  26563  cxpsqrt  26685  dvcncxp1  26725  cubic2  26830  quart1  26838  asinsinlem  26873  asinsin  26874  2efiatan  26900  pclogsum  27196  lgsneg  27302  bdayfinbndlem1  28477  vc0  30663  vcm  30665  nvpi  30756  honegneg  31895  opsqrlem6  32234  sto1i  32325  mdexchi  32424  fmptunsnop  32792  preiman0  32802  elrspunidl  33511  cnre2csqlem  34094  itgexpif  34790  subfacp1lem1  35407  rankaltopb  36207  poimirlem23  38010  dvtan  38037  dvasin  38071  heiborlem6  38183  trlcoat  41215  cdlemk54  41450  readvcot  42841  resubid  42886  sn-mul02  42942  iocunico  43656  relintab  44027  rfovcnvf1od  44448  ntrneifv3  44526  ntrneifv4  44529  clsneifv3  44554  clsneifv4  44555  neicvgfv  44565  snunioo1  45957  dvsinexp  46354  dvnprodlem1  46389  itgsubsticclem  46418  stirlinglem1  46517  fourierdlem80  46629  fourierdlem111  46660  sqwvfoura  46671  sqwvfourb  46672  fouriersw  46674  saliinclf  46769  smfco  47245  2oppf  49622  aacllem  50291