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

Theorem syl5req 2486
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1  |-  A  =  B
syl5req.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5req  |-  ( ph  ->  C  =  A )

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3  |-  A  =  B
2 syl5req.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2syl5eq 2485 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2446 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  syl5reqr  2488  opeqsn  4584  ordintdif  4764  relop  4986  funopg  5447  funcnvres  5484  csbriota  6062  nneob  7087  sucdom2  7503  unblem2  7561  pwfilem  7601  kmlem2  8316  kmlem11  8325  kmlem12  8326  cflim3  8427  1idsr  9261  recextlem1  9962  nn0suppOLD  10630  quoremz  11690  quoremnn0ALT  11692  intfrac2  11693  hashprg  12151  hashfacen  12203  leiso  12208  swrdccat3a  12381  repsw2  12546  repsw3  12547  cvgcmpce  13277  explecnv  13323  ramub1lem1  14083  ressress  14231  subsubc  14759  psgnunilem1  15992  psgn0fv0  16010  efginvrel2  16217  efgredleme  16233  efgcpbllemb  16245  frgpnabllem1  16344  gsumzaddlem  16401  gsumzmhm  16422  gsumzmhmOLD  16423  dprd2da  16531  dpjcntz  16541  dpjdisj  16542  dpjlsm  16543  dpjidcl  16547  dpjidclOLD  16554  ablfac1lem  16559  ablfac1eu  16564  lmhmlsp  17108  mplmon2mul  17559  frlmip  18162  1marepvmarrepid  18345  cramerimplem2  18449  neitr  18743  fixufil  19454  trust  19763  restmetu  20121  nmfval2  20142  nmval2  20143  rerest  20340  xrrest  20343  xrge0gsumle  20369  rrxip  20853  voliunlem3  20992  volsup  20996  itg1addlem5  21137  itg2monolem1  21187  itg2cnlem2  21199  itgmpt  21219  iblcnlem1  21224  itgcnlem  21226  itgioo  21252  limcres  21320  mdegfval  21490  dgrlem  21656  coeidlem  21664  mcubic  22201  binom4  22204  dquartlem2  22206  amgm  22343  wilthlem2  22366  rpvmasum2  22720  pntlemo  22815  wlkntrllem3  23395  opidon2  23746  vc2  23868  nvge0  23997  nmoo0  24126  bcsiALT  24516  pjchi  24770  shjshseli  24831  spanpr  24918  pjinvari  25530  mdslmd1lem2  25665  iundifdifd  25847  iundifdif  25848  gtiso  25931  rngurd  26191  esumpr2  26453  eulerpartlemt  26684  ofcccat  26872  lgamgulmlem2  26946  eflgam  26961  risefallfac  27456  dvasin  28405  dvacos  28406  topjoin  28511  tailfval  28518  tailf  28521  elrfi  28955  fzsplit1nn0  29017  rabdiophlem2  29065  eldioph4b  29075  diophren  29077  pell1qrgaplem  29139  rngunsnply  29455  compne  29621  fmuldfeq  29689  stoweidlem44  29764  fsumsplitsndif  30163  frgrancvvdeqlem4  30551  psgnsn  30688  m1detdiag  30775  cdleme4  33604  cdleme22e  33710  cdleme22eALTN  33711  cdleme42a  33837  cdleme42d  33839  cdlemk20  34240  dih1dimatlem0  34695  lcfrlem2  34910
  Copyright terms: Public domain W3C validator