Theorem 3eqtr3a 2804

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  uneqin  4308  coi2  6294  foima  6839  f1imacnv  6878  fvsnun1  7216  fnsnsplit  7218  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  rankopb  9921  fin4en1  10378  fpwwe2  10712  winacard  10761  mul02lem1  11466  cnegex2  11472  crreczi  14277  hashinf  14384  hashcard  14404  cshw0  14842  cshwn  14845  sqrtneglem  15315  rlimresb  15611  bpoly3  16106  bpoly4  16107  sinhval  16202  coshval  16203  absefib  16246  efieq1re  16247  sadcaddlem  16503  sadaddlem  16512  qus0subgbas  19238  psgnsn  19562  odngen  19619  frlmup3  21843  mat0op  22446  restopnb  23204  cnmpt2t  23702  clmnegneg  25156  ncvspi  25209  volsup2  25659  plypf1  26271  pige3ALT  26580  sineq0  26584  eflog  26636  logef  26641  cxpsqrt  26763  dvcncxp1  26803  cubic2  26909  quart1  26917  asinsinlem  26952  asinsin  26953  2efiatan  26979  pclogsum  27277  lgsneg  27383  vc0  30606  vcm  30608  nvpi  30699  honegneg  31838  opsqrlem6  32177  sto1i  32268  mdexchi  32367  preiman0  32721  elrspunidl  33421  cnre2csqlem  33856  itgexpif  34583  subfacp1lem1  35147  rankaltopb  35943  poimirlem23  37603  dvtan  37630  dvasin  37664  heiborlem6  37776  trlcoat  40680  cdlemk54  40915  resubid  42384  sn-mul02  42416  iocunico  43172  relintab  43545  rfovcnvf1od  43966  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  snunioo1  45430  dvsinexp  45832  itgsubsticclem  45896  stirlinglem1  45995  fourierdlem80  46107  fourierdlem111  46138  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  saliinclf  46247  smfco  46723  aacllem  48895