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  4248  coi2  6224  foima  6759  f1imacnv  6798  fvsnun1  7138  fnsnsplit  7140  phplem2  9146  php3  9150  rankopb  9781  fin4en1  10238  fpwwe2  10572  winacard  10621  mul02lem1  11326  cnegex2  11332  crreczi  14169  hashinf  14276  hashcard  14296  cshw0  14735  cshwn  14738  sqrtneglem  15208  rlimresb  15507  bpoly3  16000  bpoly4  16001  sinhval  16098  coshval  16099  absefib  16142  efieq1re  16143  sadcaddlem  16403  sadaddlem  16412  qus0subgbas  19106  psgnsn  19426  odngen  19483  frlmup3  21685  mat0op  22282  restopnb  23038  cnmpt2t  23536  clmnegneg  24980  ncvspi  25032  volsup2  25482  plypf1  26093  pige3ALT  26405  sineq0  26409  eflog  26461  logef  26466  cxpsqrt  26588  dvcncxp1  26628  cubic2  26734  quart1  26742  asinsinlem  26777  asinsin  26778  2efiatan  26804  pclogsum  27102  lgsneg  27208  vc0  30476  vcm  30478  nvpi  30569  honegneg  31708  opsqrlem6  32047  sto1i  32138  mdexchi  32237  fmptunsnop  32596  preiman0  32606  elrspunidl  33372  cnre2csqlem  33873  itgexpif  34570  subfacp1lem1  35139  rankaltopb  35940  poimirlem23  37610  dvtan  37637  dvasin  37671  heiborlem6  37783  trlcoat  40690  cdlemk54  40925  readvcot  42325  resubid  42370  sn-mul02  42413  iocunico  43173  relintab  43545  rfovcnvf1od  43966  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  snunioo1  45483  dvsinexp  45882  dvnprodlem1  45917  itgsubsticclem  45946  stirlinglem1  46045  fourierdlem80  46157  fourierdlem111  46188  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  saliinclf  46297  smfco  46773  2oppf  49094  aacllem  49763