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

Theorem 3eqtr3a 2709
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 2697 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2687 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  uneqin  3911  coi2  5690  foima  6158  f1imacnv  6191  fvsnun2  6490  fnsnsplit  6491  phplem4  8183  php3  8187  rankopb  8753  fin4en1  9169  fpwwe2  9503  winacard  9552  mul02lem1  10250  cnegex2  10256  crreczi  13029  hashinf  13162  hashcard  13184  cshw0  13586  cshwn  13589  sqrtneglem  14051  rlimresb  14340  bpoly3  14833  bpoly4  14834  sinhval  14928  coshval  14929  absefib  14972  efieq1re  14973  sadcaddlem  15226  sadaddlem  15235  psgnsn  17986  odngen  18038  frlmup3  20187  mat0op  20273  restopnb  21027  cnmpt2t  21524  clmnegneg  22950  ncvspi  23002  volsup2  23419  plypf1  24013  pige3  24314  sineq0  24318  eflog  24368  logef  24373  cxpsqrt  24494  dvcncxp1  24529  cubic2  24620  quart1  24628  asinsinlem  24663  asinsin  24664  2efiatan  24690  pclogsum  24985  lgsneg  25091  vc0  27557  vcm  27559  nvpi  27650  honegneg  28793  opsqrlem6  29132  sto1i  29223  mdexchi  29322  cnre2csqlem  30084  itgexpif  30812  subfacp1lem1  31287  rankaltopb  32211  poimirlem23  33562  dvtan  33590  dvasin  33626  heiborlem6  33745  trlcoat  36328  cdlemk54  36563  iocunico  38113  relintab  38206  rfovcnvf1od  38615  ntrneifv3  38697  ntrneifv4  38700  clsneifv3  38725  clsneifv4  38726  neicvgfv  38736  snunioo1  40056  dvsinexp  40443  itgsubsticclem  40509  stirlinglem1  40609  fourierdlem80  40721  fourierdlem111  40752  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  aacllem  42875
  Copyright terms: Public domain W3C validator