Theorem 3eqtr3a 2795

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  uneqin  4241  coi2  6222  foima  6751  f1imacnv  6790  fvsnun1  7128  fnsnsplit  7130  phplem2  9129  php3  9133  rankopb  9764  fin4en1  10219  fpwwe2  10554  winacard  10603  mul02lem1  11309  cnegex2  11315  crreczi  14151  hashinf  14258  hashcard  14278  cshw0  14717  cshwn  14720  sqrtneglem  15189  rlimresb  15488  bpoly3  15981  bpoly4  15982  sinhval  16079  coshval  16080  absefib  16123  efieq1re  16124  sadcaddlem  16384  sadaddlem  16393  qus0subgbas  19127  psgnsn  19449  odngen  19506  frlmup3  21755  mat0op  22363  restopnb  23119  cnmpt2t  23617  clmnegneg  25060  ncvspi  25112  volsup2  25562  plypf1  26173  pige3ALT  26485  sineq0  26489  eflog  26541  logef  26546  cxpsqrt  26668  dvcncxp1  26708  cubic2  26814  quart1  26822  asinsinlem  26857  asinsin  26858  2efiatan  26884  pclogsum  27182  lgsneg  27288  bdayfinbndlem1  28463  vc0  30649  vcm  30651  nvpi  30742  honegneg  31881  opsqrlem6  32220  sto1i  32311  mdexchi  32410  fmptunsnop  32779  preiman0  32789  elrspunidl  33509  cnre2csqlem  34067  itgexpif  34763  subfacp1lem1  35373  rankaltopb  36173  poimirlem23  37844  dvtan  37871  dvasin  37905  heiborlem6  38017  trlcoat  40983  cdlemk54  41218  readvcot  42619  resubid  42664  sn-mul02  42707  iocunico  43453  relintab  43824  rfovcnvf1od  44245  ntrneifv3  44323  ntrneifv4  44326  clsneifv3  44351  clsneifv4  44352  neicvgfv  44362  snunioo1  45758  dvsinexp  46155  dvnprodlem1  46190  itgsubsticclem  46219  stirlinglem1  46318  fourierdlem80  46430  fourierdlem111  46461  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  saliinclf  46570  smfco  47046  2oppf  49377  aacllem  50046