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

Theorem syl5req 2873
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1 𝐴 = 𝐵
syl5req.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5req (𝜑𝐶 = 𝐴)

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3 𝐴 = 𝐵
2 syl5req.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2syl5eq 2872 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2831 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818
This theorem is referenced by:  syl5reqr  2875  opeqsng  5389  relop  5719  ordintdif  6237  iotanul  6330  funopg  6385  funcnvres  6428  fpropnf1  7022  csbriota  7124  csbov123  7193  mpocurryd  7929  nneob  8272  sucdom2  8706  unblem2  8763  pwfilem  8810  kmlem2  9569  kmlem11  9578  kmlem12  9579  cflim3  9676  1idsr  10512  recextlem1  11262  quoremz  13216  quoremnn0ALT  13218  intfrac2  13219  hashprg  13749  hashfacen  13805  leiso  13810  ccatrid  13934  repsw2  14305  repsw3  14306  cvgcmpce  15166  explecnv  15213  risefallfac  15371  ramub1lem1  16355  ressress  16555  subsubc  17116  grp1inv  18140  psgnunilem1  18544  psgn0fv0  18562  psgnsn  18571  efginvrel2  18776  efgredleme  18792  efgcpbllemb  18804  frgpnabllem1  18916  gsumzaddlem  18964  gsumzmhm  18980  fsfnn0gsumfsffz  19026  dprd2da  19087  dpjcntz  19097  dpjdisj  19098  dpjlsm  19099  dpjidcl  19103  ablfac1lem  19113  ablfac1eu  19118  rnrhmsubrg  19490  lmhmlsp  19744  mplmon2mul  20202  frlmip  20841  1marepvmarrepid  21103  m1detdiag  21125  cramerimplem2  21212  pmatcollpw3lem  21310  chpscmatgsumbin  21371  chpscmatgsummon  21372  cayhamlem2  21411  neitr  21707  fixufil  22449  trust  22756  restmetu  23098  nmfval2  23118  nmval2  23119  rerest  23330  xrrest  23333  xrge0gsumle  23359  rrxip  23911  rrx0  23918  rrxdsfi  23932  voliunlem3  24071  volsup  24075  itg1addlem5  24219  itg2monolem1  24269  itg2cnlem2  24281  itgmpt  24301  iblcnlem1  24306  itgcnlem  24308  itgioo  24334  limcres  24402  mdegfval  24574  dgrlem  24737  coeidlem  24745  mcubic  25341  binom4  25344  dquartlem2  25346  amgm  25485  lgamgulmlem2  25524  eflgam  25539  wilthlem2  25563  rpvmasum2  26005  pntlemo  26100  wlkres  27369  3wlkond  27867  3cycld  27874  frgrncvvdeqlem3  27997  vc2OLD  28262  nvge0  28367  nmoo0  28485  bcsiALT  28873  pjchi  29126  shjshseli  29187  spanpr  29274  pjinvari  29885  mdslmd1lem2  30020  iundifdifd  30231  iundifdif  30232  fmptco1f1o  30296  gtiso  30352  cycpmco2lem4  30688  cycpmconjslem2  30714  rngurd  30774  rspsnel  30853  esumpr2  31215  omssubaddlem  31446  eulerpartlemt  31518  ofcccat  31702  2cycld  32272  satfv1lem  32496  topjoin  33600  tailfval  33607  tailf  33610  dvasin  34848  dvacos  34849  opidon2OLD  35003  cdleme4  37244  cdleme22e  37350  cdleme22eALTN  37351  cdleme42a  37477  cdleme42d  37479  cdlemk20  37880  dih1dimatlem0  38334  lcfrlem2  38549  prjspnval2  39135  elrfi  39159  fzsplit1nn0  39219  rabdiophlem2  39267  eldioph4b  39276  diophren  39278  pell1qrgaplem  39338  rngunsnply  39641  fmuldfeq  41732  limciccioolb  41770  ditgeq3d  42117  stoweidlem44  42198  dirkertrigeq  42255  fourierdlem32  42293  fourierdlem33  42294  fourierdlem42  42303  fourierdlem62  42322  fourierdlem84  42344  fourierdlem85  42345  fourierdlem97  42357  fourierdlem98  42358  fourierdlem102  42362  fourierdlem104  42364  fourierdlem113  42373  fourierdlem114  42374  fourierswlem  42384  fouriersw  42385  sssalgen  42487  meadjun  42613  deccarry  43380  fsumsplitsndif  43402  isomushgr  43826  ushrisomgr  43841  funcrngcsetcALT  44105  2sphere  44571
  Copyright terms: Public domain W3C validator