Theorem 3eqtr3a 2880

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  uneqin  4254  coi2  6110  foima  6589  f1imacnv  6625  fvsnun1  6938  fnsnsplit  6940  phplem4  8693  php3  8697  rankopb  9275  fin4en1  9725  fpwwe2  10059  winacard  10108  mul02lem1  10810  cnegex2  10816  crreczi  13583  hashinf  13689  hashcard  13710  cshw0  14150  cshwn  14153  sqrtneglem  14620  rlimresb  14916  bpoly3  15406  bpoly4  15407  sinhval  15501  coshval  15502  absefib  15545  efieq1re  15546  sadcaddlem  15800  sadaddlem  15809  psgnsn  18642  odngen  18696  frlmup3  20938  mat0op  21022  restopnb  21777  cnmpt2t  22275  clmnegneg  23702  ncvspi  23754  volsup2  24200  plypf1  24796  pige3ALT  25099  sineq0  25103  eflog  25154  logef  25159  cxpsqrt  25280  dvcncxp1  25318  cubic2  25420  quart1  25428  asinsinlem  25463  asinsin  25464  2efiatan  25490  pclogsum  25785  lgsneg  25891  vc0  28345  vcm  28347  nvpi  28438  honegneg  29577  opsqrlem6  29916  sto1i  30007  mdexchi  30106  cnre2csqlem  31148  itgexpif  31872  subfacp1lem1  32421  rankaltopb  33435  poimirlem23  34909  dvtan  34936  dvasin  34972  heiborlem6  35088  trlcoat  37853  cdlemk54  38088  resubid  39231  iocunico  39810  relintab  39936  rfovcnvf1od  40343  ntrneifv3  40425  ntrneifv4  40428  clsneifv3  40453  clsneifv4  40454  neicvgfv  40464  snunioo1  41781  dvsinexp  42188  itgsubsticclem  42253  stirlinglem1  42353  fourierdlem80  42465  fourierdlem111  42496  sqwvfoura  42507  sqwvfourb  42508  fouriersw  42510  aacllem  44896