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

Theorem 3eqtr3a 2522
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 2510 . 2
51, 4eqtr3d 2500 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395
This theorem is referenced by:  uneqin  3748  coi2  5529  foima  5805  f1imacnv  5837  fvsnun2  6107  fnsnsplit  6108  phplem4  7719  php3  7723  rankopb  8291  fin4en1  8710  fpwwe2  9042  winacard  9091  mul02lem1  9777  cnegex2  9783  crreczi  12291  hashinf  12410  hashcard  12427  cshw0  12765  cshwn  12768  sqrtneglem  13100  rlimresb  13388  sinhval  13889  coshval  13890  absefib  13933  efieq1re  13934  sadcaddlem  14107  sadaddlem  14116  psgnsn  16545  odngen  16597  frlmup3  18834  mat0op  18921  restopnb  19676  cnmpt2t  20174  volsup2  22014  plypf1  22609  pige3  22910  sineq0  22914  eflog  22964  logef  22966  cxpsqrt  23084  cubic2  23179  quart1  23187  asinsinlem  23222  asinsin  23223  2efiatan  23249  pclogsum  23490  lgsneg  23594  numclwlk1lem2fo  25095  vc0  25462  vcm  25464  vcnegneg  25467  nvpi  25569  honegneg  26725  opsqrlem6  27064  sto1i  27155  mdexchi  27254  cnre2csqlem  27892  subfacp1lem1  28623  ghomfo  29031  rankaltopb  29629  bpoly3  29820  bpoly4  29821  dvtan  30065  dvcncxp1  30100  dvasin  30103  heiborlem6  30312  iocunico  31178  snunioo1  31552  dvsinexp  31705  itgsubsticclem  31774  stirlinglem1  31856  fourierdlem80  31969  fourierdlem111  32000  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  aacllem  33216  trlcoat  36449  cdlemk54  36684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator