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  4240  coi2  6212  foima  6741  f1imacnv  6780  fvsnun1  7118  fnsnsplit  7120  phplem2  9119  php3  9123  rankopb  9748  fin4en1  10203  fpwwe2  10537  winacard  10586  mul02lem1  11292  cnegex2  11298  crreczi  14135  hashinf  14242  hashcard  14262  cshw0  14700  cshwn  14703  sqrtneglem  15173  rlimresb  15472  bpoly3  15965  bpoly4  15966  sinhval  16063  coshval  16064  absefib  16107  efieq1re  16108  sadcaddlem  16368  sadaddlem  16377  qus0subgbas  19077  psgnsn  19399  odngen  19456  frlmup3  21707  mat0op  22304  restopnb  23060  cnmpt2t  23558  clmnegneg  25002  ncvspi  25054  volsup2  25504  plypf1  26115  pige3ALT  26427  sineq0  26431  eflog  26483  logef  26488  cxpsqrt  26610  dvcncxp1  26650  cubic2  26756  quart1  26764  asinsinlem  26799  asinsin  26800  2efiatan  26826  pclogsum  27124  lgsneg  27230  vc0  30518  vcm  30520  nvpi  30611  honegneg  31750  opsqrlem6  32089  sto1i  32180  mdexchi  32279  fmptunsnop  32642  preiman0  32652  elrspunidl  33365  cnre2csqlem  33877  itgexpif  34574  subfacp1lem1  35152  rankaltopb  35953  poimirlem23  37623  dvtan  37650  dvasin  37684  heiborlem6  37796  trlcoat  40702  cdlemk54  40937  readvcot  42337  resubid  42382  sn-mul02  42425  iocunico  43184  relintab  43556  rfovcnvf1od  43977  ntrneifv3  44055  ntrneifv4  44058  clsneifv3  44083  clsneifv4  44084  neicvgfv  44094  snunioo1  45493  dvsinexp  45892  dvnprodlem1  45927  itgsubsticclem  45956  stirlinglem1  46055  fourierdlem80  46167  fourierdlem111  46198  sqwvfoura  46209  sqwvfourb  46210  fouriersw  46212  saliinclf  46307  smfco  46783  2oppf  49117  aacllem  49786