Theorem 3eqtr3a 2788

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  uneqin  4252  coi2  6236  foima  6777  f1imacnv  6816  fvsnun1  7156  fnsnsplit  7158  phplem2  9169  php3  9173  rankopb  9805  fin4en1  10262  fpwwe2  10596  winacard  10645  mul02lem1  11350  cnegex2  11356  crreczi  14193  hashinf  14300  hashcard  14320  cshw0  14759  cshwn  14762  sqrtneglem  15232  rlimresb  15531  bpoly3  16024  bpoly4  16025  sinhval  16122  coshval  16123  absefib  16166  efieq1re  16167  sadcaddlem  16427  sadaddlem  16436  qus0subgbas  19130  psgnsn  19450  odngen  19507  frlmup3  21709  mat0op  22306  restopnb  23062  cnmpt2t  23560  clmnegneg  25004  ncvspi  25056  volsup2  25506  plypf1  26117  pige3ALT  26429  sineq0  26433  eflog  26485  logef  26490  cxpsqrt  26612  dvcncxp1  26652  cubic2  26758  quart1  26766  asinsinlem  26801  asinsin  26802  2efiatan  26828  pclogsum  27126  lgsneg  27232  vc0  30503  vcm  30505  nvpi  30596  honegneg  31735  opsqrlem6  32074  sto1i  32165  mdexchi  32264  fmptunsnop  32623  preiman0  32633  elrspunidl  33399  cnre2csqlem  33900  itgexpif  34597  subfacp1lem1  35166  rankaltopb  35967  poimirlem23  37637  dvtan  37664  dvasin  37698  heiborlem6  37810  trlcoat  40717  cdlemk54  40952  readvcot  42352  resubid  42397  sn-mul02  42440  iocunico  43200  relintab  43572  rfovcnvf1od  43993  ntrneifv3  44071  ntrneifv4  44074  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  snunioo1  45510  dvsinexp  45909  dvnprodlem1  45944  itgsubsticclem  45973  stirlinglem1  46072  fourierdlem80  46184  fourierdlem111  46215  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  saliinclf  46324  smfco  46800  2oppf  49121  aacllem  49790