MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3a Structured version   Visualization version   GIF version

Theorem 3eqtr3a 2667
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
StepHypRef Expression
1 3eqtr3a.2 . 2 (𝜑𝐴 = 𝐶)
2 3eqtr3a.1 . . 3 𝐴 = 𝐵
3 3eqtr3a.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3syl5eq 2655 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2645 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  uneqin  3836  coi2  5554  foima  6017  f1imacnv  6050  fvsnun2  6331  fnsnsplit  6332  phplem4  8004  php3  8008  rankopb  8575  fin4en1  8991  fpwwe2  9321  winacard  9370  mul02lem1  10063  cnegex2  10069  crreczi  12808  hashinf  12941  hashcard  12962  cshw0  13339  cshwn  13342  sqrtneglem  13803  rlimresb  14092  bpoly3  14576  bpoly4  14577  sinhval  14671  coshval  14672  absefib  14715  efieq1re  14716  sadcaddlem  14965  sadaddlem  14974  psgnsn  17711  odngen  17763  frlmup3  19905  mat0op  19991  restopnb  20736  cnmpt2t  21233  clmnegneg  22659  ncvspi  22708  volsup2  23123  plypf1  23716  pige3  24017  sineq0  24021  eflog  24071  logef  24076  cxpsqrt  24193  dvcncxp1  24228  cubic2  24319  quart1  24327  asinsinlem  24362  asinsin  24363  2efiatan  24389  pclogsum  24684  lgsneg  24790  numclwlk1lem2fo  26415  vc0  26606  vcm  26608  nvpi  26699  honegneg  27842  opsqrlem6  28181  sto1i  28272  mdexchi  28371  cnre2csqlem  29077  subfacp1lem1  30208  rankaltopb  31049  poimirlem23  32385  dvtan  32413  dvasin  32449  heiborlem6  32568  trlcoat  34812  cdlemk54  35047  iocunico  36598  relintab  36691  rfovcnvf1od  37101  ntrneifv3  37183  ntrneifv4  37186  clsneifv3  37211  clsneifv4  37212  neicvgfv  37222  snunioo1  38368  dvsinexp  38581  itgsubsticclem  38650  stirlinglem1  38750  fourierdlem80  38862  fourierdlem111  38893  sqwvfoura  38904  sqwvfourb  38905  fouriersw  38907  av-numclwlk1lem2fo  41506  aacllem  42298
  Copyright terms: Public domain W3C validator