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

Theorem syl5req 2488
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 2487 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2448 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  syl5reqr  2490  opeqsn  4592  ordintdif  4773  relop  4995  funopg  5455  funcnvres  5492  csbriota  6069  mpt2curryd  6793  nneob  7096  sucdom2  7512  unblem2  7570  pwfilem  7610  kmlem2  8325  kmlem11  8334  kmlem12  8335  cflim3  8436  1idsr  9270  recextlem1  9971  nn0suppOLD  10639  quoremz  11699  quoremnn0ALT  11701  intfrac2  11702  hashprg  12160  hashfacen  12212  leiso  12217  swrdccat3a  12390  repsw2  12555  repsw3  12556  cvgcmpce  13286  explecnv  13332  ramub1lem1  14092  ressress  14240  subsubc  14768  psgnunilem1  16004  psgn0fv0  16022  efginvrel2  16229  efgredleme  16245  efgcpbllemb  16257  frgpnabllem1  16356  gsumzaddlem  16413  gsumzmhm  16435  gsumzmhmOLD  16436  dprd2da  16546  dpjcntz  16556  dpjdisj  16557  dpjlsm  16558  dpjidcl  16562  dpjidclOLD  16569  ablfac1lem  16574  ablfac1eu  16579  lmhmlsp  17135  mplmon2mul  17588  frlmip  18208  1marepvmarrepid  18391  cramerimplem2  18495  neitr  18789  fixufil  19500  trust  19809  restmetu  20167  nmfval2  20188  nmval2  20189  rerest  20386  xrrest  20389  xrge0gsumle  20415  rrxip  20899  voliunlem3  21038  volsup  21042  itg1addlem5  21183  itg2monolem1  21233  itg2cnlem2  21245  itgmpt  21265  iblcnlem1  21270  itgcnlem  21272  itgioo  21298  limcres  21366  mdegfval  21536  dgrlem  21702  coeidlem  21710  mcubic  22247  binom4  22250  dquartlem2  22252  amgm  22389  wilthlem2  22412  rpvmasum2  22766  pntlemo  22861  wlkntrllem3  23465  opidon2  23816  vc2  23938  nvge0  24067  nmoo0  24196  bcsiALT  24586  pjchi  24840  shjshseli  24901  spanpr  24988  pjinvari  25600  mdslmd1lem2  25735  iundifdifd  25917  iundifdif  25918  gtiso  26001  rngurd  26261  esumpr2  26522  eulerpartlemt  26759  ofcccat  26947  lgamgulmlem2  27021  eflgam  27036  risefallfac  27532  dvasin  28485  dvacos  28486  topjoin  28591  tailfval  28598  tailf  28601  elrfi  29035  fzsplit1nn0  29097  rabdiophlem2  29145  eldioph4b  29155  diophren  29157  pell1qrgaplem  29219  rngunsnply  29535  compne  29701  fmuldfeq  29769  stoweidlem44  29844  fsumsplitsndif  30243  frgrancvvdeqlem4  30631  psgnsn  30776  fsfnn0gsumfsffz  30808  m1detdiag  30939  cdleme4  33887  cdleme22e  33993  cdleme22eALTN  33994  cdleme42a  34120  cdleme42d  34122  cdlemk20  34523  dih1dimatlem0  34978  lcfrlem2  35193
  Copyright terms: Public domain W3C validator