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

Theorem 3eqtr3a 2668
 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 2656 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2646 1 (𝜑𝐶 = 𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603 This theorem is referenced by:  uneqin  3837  coi2  5569  foima  6033  f1imacnv  6066  fvsnun2  6354  fnsnsplit  6355  phplem4  8027  php3  8031  rankopb  8598  fin4en1  9014  fpwwe2  9344  winacard  9393  mul02lem1  10091  cnegex2  10097  crreczi  12851  hashinf  12984  hashcard  13008  cshw0  13391  cshwn  13394  sqrtneglem  13855  rlimresb  14144  bpoly3  14628  bpoly4  14629  sinhval  14723  coshval  14724  absefib  14767  efieq1re  14768  sadcaddlem  15017  sadaddlem  15026  psgnsn  17763  odngen  17815  frlmup3  19958  mat0op  20044  restopnb  20789  cnmpt2t  21286  clmnegneg  22712  ncvspi  22764  volsup2  23179  plypf1  23772  pige3  24073  sineq0  24077  eflog  24127  logef  24132  cxpsqrt  24249  dvcncxp1  24284  cubic2  24375  quart1  24383  asinsinlem  24418  asinsin  24419  2efiatan  24445  pclogsum  24740  lgsneg  24846  numclwlk1lem2fo  26622  vc0  26813  vcm  26815  nvpi  26906  honegneg  28049  opsqrlem6  28388  sto1i  28479  mdexchi  28578  cnre2csqlem  29284  subfacp1lem1  30415  rankaltopb  31256  poimirlem23  32602  dvtan  32630  dvasin  32666  heiborlem6  32785  trlcoat  35029  cdlemk54  35264  iocunico  36815  relintab  36908  rfovcnvf1od  37318  ntrneifv3  37400  ntrneifv4  37403  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439  snunioo1  38585  dvsinexp  38798  itgsubsticclem  38867  stirlinglem1  38967  fourierdlem80  39079  fourierdlem111  39110  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  av-numclwlk1lem2fo  41525  aacllem  42356
 Copyright terms: Public domain W3C validator