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

Theorem syl5req 2483
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 2482 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2437 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  syl5reqr  2485  opeqsn  4717  relop  5005  ordintdif  5491  funopg  5633  funcnvres  5670  csbriota  6279  csbov123  6339  mpt2curryd  7024  nneob  7361  sucdom2  7774  unblem2  7830  pwfilem  7874  kmlem2  8579  kmlem11  8588  kmlem12  8589  cflim3  8690  1idsr  9521  recextlem1  10241  quoremz  12079  quoremnn0ALT  12081  intfrac2  12082  hashprg  12569  hashfacen  12612  leiso  12617  ccatrid  12718  swrdccat3a  12835  repsw2  13004  repsw3  13005  cvgcmpce  13856  explecnv  13901  risefallfac  14055  ramub1lem1  14947  ressress  15149  subsubc  15709  psgnunilem1  17085  psgn0fv0  17103  psgnsn  17112  efginvrel2  17312  efgredleme  17328  efgcpbllemb  17340  frgpnabllem1  17444  gsumzaddlem  17489  gsumzmhm  17505  fsfnn0gsumfsffz  17547  dprd2da  17610  dpjcntz  17620  dpjdisj  17621  dpjlsm  17622  dpjidcl  17626  ablfac1lem  17636  ablfac1eu  17641  lmhmlsp  18207  mplmon2mul  18659  frlmip  19267  1marepvmarrepid  19531  m1detdiag  19553  cramerimplem2  19640  pmatcollpw3lem  19738  chpscmatgsumbin  19799  chpscmatgsummon  19800  cayhamlem2  19839  neitr  20127  fixufil  20868  trust  21175  restmetu  21516  nmfval2  21536  nmval2  21537  rerest  21733  xrrest  21736  xrge0gsumle  21762  rrxip  22242  voliunlem3  22382  volsup  22386  itg1addlem5  22535  itg2monolem1  22585  itg2cnlem2  22597  itgmpt  22617  iblcnlem1  22622  itgcnlem  22624  itgioo  22650  limcres  22718  mdegfval  22888  dgrlem  23051  coeidlem  23059  mcubic  23638  binom4  23641  dquartlem2  23643  amgm  23781  lgamgulmlem2  23820  eflgam  23835  wilthlem2  23859  rpvmasum2  24213  pntlemo  24308  wlkntrllem3  25136  frgrancvvdeqlem4  25606  opidon2OLD  25897  vc2  26019  nvge0  26148  nmoo0  26277  bcsiALT  26667  pjchi  26920  shjshseli  26981  spanpr  27068  pjinvari  27679  mdslmd1lem2  27814  iundifdifd  28016  iundifdif  28017  gtiso  28121  rngurd  28390  esumpr2  28727  eulerpartlemt  29030  ofcccat  29218  topjoin  30806  tailfval  30813  tailf  30816  dvasin  31732  dvacos  31733  cdleme4  33513  cdleme22e  33620  cdleme22eALTN  33621  cdleme42a  33747  cdleme42d  33749  cdlemk20  34150  dih1dimatlem0  34605  lcfrlem2  34820  elrfi  35245  fzsplit1nn0  35305  rabdiophlem2  35354  eldioph4b  35363  diophren  35365  pell1qrgaplem  35427  rngunsnply  35738  compne  36430  fmuldfeq  37233  limciccioolb  37273  ditgeq3d  37410  stoweidlem44  37474  dirkertrigeq  37532  fourierdlem32  37570  fourierdlem33  37571  fourierdlem42  37580  fourierdlem62  37600  fourierdlem84  37622  fourierdlem85  37623  fourierdlem97  37635  fourierdlem98  37636  fourierdlem102  37640  fourierdlem104  37642  fourierdlem113  37651  fourierdlem114  37652  fourierswlem  37662  fouriersw  37663  meadjun  37809  deccarry  38105  fsumsplitsndif  38416  funcrngcsetcALT  38759
  Copyright terms: Public domain W3C validator