Theorem 3eqtr3a 2824

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  uneqin  4242  coi2  6267  foima  6801  f1imacnv  6841  fvsnun1  7186  fnsnsplit  7188  phplem2  9196  php3  9200  rankopb  9831  fin4en1  10308  fpwwe2  10643  winacard  10692  mul02lem1  11401  cnegex2  11407  crreczi  14282  hashinf  14389  hashcard  14409  cshw0  14855  cshwn  14858  sqrtneglem  15341  rlimresb  15640  bpoly3  16134  bpoly4  16135  sinhval  16232  coshval  16233  absefib  16276  efieq1re  16277  sadcaddlem  16537  sadaddlem  16546  qus0subgbas  19313  psgnsn  19634  odngen  19691  frlmup3  22000  mat0op  22626  restopnb  23382  cnmpt2t  23881  clmnegneg  25314  ncvspi  25366  volsup2  25815  plypf1  26420  pige3ALT  26736  sineq0  26740  eflog  26792  logef  26797  cxpsqrt  26919  dvcncxp1  26959  cubic2  27064  quart1  27072  asinsinlem  27107  asinsin  27108  2efiatan  27134  pclogsum  27430  lgsneg  27536  bdayfinbndlem1  28711  vc0  30997  vcm  30999  nvpi  31090  honegneg  32229  opsqrlem6  32568  sto1i  32659  mdexchi  32758  fmptunsnop  33116  preiman0  33126  elrspunidl  33800  cnre2csqlem  34364  itgexpif  35058  subfacp1lem1  35708  rankaltopb  36508  poimirlem23  38351  dvtan  38378  dvasin  38412  heiborlem6  38525  trlcoat  41555  cdlemk54  41790  readvcot  43183  resubid  43228  sn-mul02  43284  iocunico  43996  relintab  44367  rfovcnvf1od  44788  ntrneifv3  44866  ntrneifv4  44869  clsneifv3  44894  clsneifv4  44895  neicvgfv  44905  snunioo1  46286  dvsinexp  46683  dvnprodlem1  46718  itgsubsticclem  46747  stirlinglem1  46846  fourierdlem80  46958  fourierdlem111  46989  sqwvfoura  47000  sqwvfourb  47001  fouriersw  47003  saliinclf  47098  smfco  47574  2oppf  49967  aacllem  50678