MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5req Structured 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 2462 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  syl5reqr  2510  opeqsn  4732  ordintdif  4916  relop  5142  funopg  5602  funcnvres  5639  csbriota  6244  csbov123  6304  mpt2curryd  6990  nneob  7293  sucdom2  7707  unblem2  7765  pwfilem  7806  kmlem2  8522  kmlem11  8531  kmlem12  8532  cflim3  8633  1idsr  9464  recextlem1  10175  nn0suppOLD  10846  quoremz  11964  quoremnn0ALT  11966  intfrac2  11967  hashprg  12447  hashfacen  12490  leiso  12495  ccatrid  12596  swrdccat3a  12713  repsw2  12882  repsw3  12883  cvgcmpce  13717  explecnv  13761  ramub1lem1  14631  ressress  14784  subsubc  15344  psgnunilem1  16720  psgn0fv0  16738  psgnsn  16747  efginvrel2  16947  efgredleme  16963  efgcpbllemb  16975  frgpnabllem1  17079  gsumzaddlem  17136  gsumzmhm  17158  gsumzmhmOLD  17159  fsfnn0gsumfsffz  17209  dprd2da  17289  dpjcntz  17299  dpjdisj  17300  dpjlsm  17301  dpjidcl  17305  dpjidclOLD  17312  ablfac1lem  17317  ablfac1eu  17322  lmhmlsp  17893  mplmon2mul  18364  frlmip  18983  1marepvmarrepid  19247  m1detdiag  19269  cramerimplem2  19356  pmatcollpw3lem  19454  chpscmatgsumbin  19515  chpscmatgsummon  19516  cayhamlem2  19555  neitr  19851  fixufil  20592  trust  20901  restmetu  21259  nmfval2  21280  nmval2  21281  rerest  21478  xrrest  21481  xrge0gsumle  21507  rrxip  21991  voliunlem3  22131  volsup  22135  itg1addlem5  22276  itg2monolem1  22326  itg2cnlem2  22338  itgmpt  22358  iblcnlem1  22363  itgcnlem  22365  itgioo  22391  limcres  22459  mdegfval  22629  dgrlem  22795  coeidlem  22803  mcubic  23378  binom4  23381  dquartlem2  23383  amgm  23521  wilthlem2  23544  rpvmasum2  23898  pntlemo  23993  wlkntrllem3  24768  frgrancvvdeqlem4  25238  opidon2OLD  25527  vc2  25649  nvge0  25778  nmoo0  25907  bcsiALT  26297  pjchi  26551  shjshseli  26612  spanpr  26699  pjinvari  27311  mdslmd1lem2  27446  iundifdifd  27642  iundifdif  27643  gtiso  27750  rngurd  28016  esumpr2  28299  eulerpartlemt  28577  ofcccat  28765  lgamgulmlem2  28839  eflgam  28854  risefallfac  29390  dvasin  30346  dvacos  30347  topjoin  30426  tailfval  30433  tailf  30436  elrfi  30869  fzsplit1nn0  30929  rabdiophlem2  30978  eldioph4b  30987  diophren  30989  pell1qrgaplem  31051  rngunsnply  31366  compne  31593  fmuldfeq  31819  limciccioolb  31869  ditgeq3d  32005  stoweidlem44  32068  dirkertrigeq  32125  fourierdlem32  32163  fourierdlem33  32164  fourierdlem42  32173  fourierdlem62  32193  fourierdlem84  32215  fourierdlem85  32216  fourierdlem97  32228  fourierdlem98  32229  fourierdlem102  32233  fourierdlem104  32235  fourierdlem113  32244  fourierdlem114  32245  fourierswlem  32255  fouriersw  32256  fsumsplitsndif  32737  funcrngcsetcALT  33080  cdleme4  36379  cdleme22e  36486  cdleme22eALTN  36487  cdleme42a  36613  cdleme42d  36615  cdlemk20  37016  dih1dimatlem0  37471  lcfrlem2  37686
  Copyright terms: Public domain W3C validator