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

Theorem syl5req 2508
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 2507 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2467 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454
This theorem is referenced by:  syl5reqr  2510  opeqsn  4710  relop  5003  ordintdif  5490  funopg  5632  funcnvres  5673  csbriota  6288  csbov123  6348  mpt2curryd  7041  nneob  7378  sucdom2  7793  unblem2  7849  pwfilem  7893  kmlem2  8606  kmlem11  8615  kmlem12  8616  cflim3  8717  1idsr  9547  recextlem1  10269  quoremz  12113  quoremnn0ALT  12115  intfrac2  12116  hashprg  12603  hashfacen  12649  leiso  12654  ccatrid  12766  swrdccat3a  12886  repsw2  13073  repsw3  13074  cvgcmpce  13926  explecnv  13971  risefallfac  14125  ramub1lem1  15032  ressress  15235  subsubc  15806  psgnunilem1  17182  psgn0fv0  17200  psgnsn  17209  efginvrel2  17425  efgredleme  17441  efgcpbllemb  17453  frgpnabllem1  17557  gsumzaddlem  17602  gsumzmhm  17618  fsfnn0gsumfsffz  17660  dprd2da  17723  dpjcntz  17733  dpjdisj  17734  dpjlsm  17735  dpjidcl  17739  ablfac1lem  17749  ablfac1eu  17754  lmhmlsp  18320  mplmon2mul  18772  frlmip  19384  1marepvmarrepid  19648  m1detdiag  19670  cramerimplem2  19757  pmatcollpw3lem  19855  chpscmatgsumbin  19916  chpscmatgsummon  19917  cayhamlem2  19956  neitr  20244  fixufil  20985  trust  21292  restmetu  21633  nmfval2  21653  nmval2  21654  rerest  21870  xrrest  21873  xrge0gsumle  21899  rrxip  22397  voliunlem3  22553  volsup  22557  itg1addlem5  22706  itg2monolem1  22756  itg2cnlem2  22768  itgmpt  22788  iblcnlem1  22793  itgcnlem  22795  itgioo  22821  limcres  22889  mdegfval  23059  dgrlem  23231  coeidlem  23239  mcubic  23821  binom4  23824  dquartlem2  23826  amgm  23964  lgamgulmlem2  24003  eflgam  24018  wilthlem2  24042  rpvmasum2  24398  pntlemo  24493  wlkntrllem3  25339  frgrancvvdeqlem4  25809  opidon2OLD  26100  vc2  26222  nvge0  26351  nmoo0  26480  bcsiALT  26880  pjchi  27133  shjshseli  27194  spanpr  27281  pjinvari  27892  mdslmd1lem2  28027  iundifdifd  28225  iundifdif  28226  gtiso  28329  rngurd  28599  esumpr2  28936  omssubaddlem  29175  eulerpartlemt  29252  ofcccat  29478  topjoin  31069  tailfval  31076  tailf  31079  dvasin  32072  dvacos  32073  cdleme4  33848  cdleme22e  33955  cdleme22eALTN  33956  cdleme42a  34082  cdleme42d  34084  cdlemk20  34485  dih1dimatlem0  34940  lcfrlem2  35155  elrfi  35580  fzsplit1nn0  35640  rabdiophlem2  35689  eldioph4b  35698  diophren  35700  pell1qrgaplem  35763  rngunsnply  36083  compne  36836  fmuldfeq  37698  limciccioolb  37738  ditgeq3d  37878  stoweidlem44  37942  dirkertrigeq  38000  fourierdlem32  38039  fourierdlem33  38040  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem62  38069  fourierdlem84  38091  fourierdlem85  38092  fourierdlem97  38104  fourierdlem98  38105  fourierdlem102  38109  fourierdlem104  38111  fourierdlem113  38120  fourierdlem114  38121  fourierswlem  38131  fouriersw  38132  sssalgen  38231  meadjun  38337  deccarry  38752  fpropnf1  39077  fsumsplitsndif  39137  1wlkvtxedg  39702  31wlkond  39911  3cycld  39918  funcrngcsetcALT  40273
  Copyright terms: Public domain W3C validator