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

Theorem 3eqtr3a 2881
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 2869 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2859 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  uneqin  4229  coi2  6094  foima  6577  f1imacnv  6613  fvsnun1  6926  fnsnsplit  6928  phplem4  8687  php3  8691  rankopb  9269  fin4en1  9720  fpwwe2  10054  winacard  10103  mul02lem1  10805  cnegex2  10811  crreczi  13585  hashinf  13691  hashcard  13712  cshw0  14147  cshwn  14150  sqrtneglem  14617  rlimresb  14913  bpoly3  15403  bpoly4  15404  sinhval  15498  coshval  15499  absefib  15542  efieq1re  15543  sadcaddlem  15795  sadaddlem  15804  psgnsn  18639  odngen  18693  frlmup3  20487  mat0op  21022  restopnb  21778  cnmpt2t  22276  clmnegneg  23707  ncvspi  23759  volsup2  24207  plypf1  24807  pige3ALT  25110  sineq0  25114  eflog  25166  logef  25171  cxpsqrt  25292  dvcncxp1  25330  cubic2  25432  quart1  25440  asinsinlem  25475  asinsin  25476  2efiatan  25502  pclogsum  25797  lgsneg  25903  vc0  28355  vcm  28357  nvpi  28448  honegneg  29587  opsqrlem6  29926  sto1i  30017  mdexchi  30116  preiman0  30453  cnre2csqlem  31227  itgexpif  31951  subfacp1lem1  32500  rankaltopb  33514  poimirlem23  35038  dvtan  35065  dvasin  35099  heiborlem6  35212  trlcoat  37977  cdlemk54  38212  resubid  39490  iocunico  40091  relintab  40213  rfovcnvf1od  40636  ntrneifv3  40718  ntrneifv4  40721  clsneifv3  40746  clsneifv4  40747  neicvgfv  40757  snunioo1  42088  dvsinexp  42492  itgsubsticclem  42556  stirlinglem1  42655  fourierdlem80  42767  fourierdlem111  42798  sqwvfoura  42809  sqwvfourb  42810  fouriersw  42812  aacllem  45268
  Copyright terms: Public domain W3C validator