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

Theorem syl5req 2698
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 2697 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2657 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  syl5reqr  2700  opeqsn  4996  relop  5305  ordintdif  5812  iotanul  5904  funopg  5960  funcnvres  6005  fpropnf1  6564  csbriota  6663  csbov123  6727  mpt2curryd  7440  nneob  7777  sucdom2  8197  unblem2  8254  pwfilem  8301  kmlem2  9011  kmlem11  9020  kmlem12  9021  cflim3  9122  1idsr  9957  recextlem1  10695  quoremz  12694  quoremnn0ALT  12696  intfrac2  12697  hashprg  13220  hashprgOLD  13221  hashfacen  13276  leiso  13281  ccatrid  13405  swrdccat3a  13540  repsw2  13739  repsw3  13740  cvgcmpce  14594  explecnv  14641  risefallfac  14799  ramub1lem1  15777  ressress  15985  subsubc  16560  grp1inv  17570  psgnunilem1  17959  psgn0fv0  17977  psgnsn  17986  efginvrel2  18186  efgredleme  18202  efgcpbllemb  18214  frgpnabllem1  18322  gsumzaddlem  18367  gsumzmhm  18383  fsfnn0gsumfsffz  18425  dprd2da  18487  dpjcntz  18497  dpjdisj  18498  dpjlsm  18499  dpjidcl  18503  ablfac1lem  18513  ablfac1eu  18518  lmhmlsp  19097  mplmon2mul  19549  frlmip  20165  1marepvmarrepid  20429  m1detdiag  20451  cramerimplem2  20538  pmatcollpw3lem  20636  chpscmatgsumbin  20697  chpscmatgsummon  20698  cayhamlem2  20737  neitr  21032  fixufil  21773  trust  22080  restmetu  22422  nmfval2  22442  nmval2  22443  rerest  22654  xrrest  22657  xrge0gsumle  22683  rrxip  23224  voliunlem3  23366  volsup  23370  itg1addlem5  23512  itg2monolem1  23562  itg2cnlem2  23574  itgmpt  23594  iblcnlem1  23599  itgcnlem  23601  itgioo  23627  limcres  23695  mdegfval  23867  dgrlem  24030  coeidlem  24038  mcubic  24619  binom4  24622  dquartlem2  24624  amgm  24762  lgamgulmlem2  24801  eflgam  24816  wilthlem2  24840  rpvmasum2  25246  pntlemo  25341  wlkres  26623  3wlkond  27149  3cycld  27156  frgrncvvdeqlem3  27281  extwwlkfablem1OLD  27323  vc2OLD  27551  nvge0  27656  nmoo0  27774  bcsiALT  28164  pjchi  28419  shjshseli  28480  spanpr  28567  pjinvari  29178  mdslmd1lem2  29313  iundifdifd  29506  iundifdif  29507  fmptco1f1o  29562  gtiso  29606  rngurd  29916  esumpr2  30257  omssubaddlem  30489  eulerpartlemt  30561  ofcccat  30748  topjoin  32485  tailfval  32492  tailf  32495  dvasin  33626  dvacos  33627  opidon2OLD  33783  cdleme4  35843  cdleme22e  35949  cdleme22eALTN  35950  cdleme42a  36076  cdleme42d  36078  cdlemk20  36479  dih1dimatlem0  36934  lcfrlem2  37149  elrfi  37574  fzsplit1nn0  37634  rabdiophlem2  37683  eldioph4b  37692  diophren  37694  pell1qrgaplem  37754  rngunsnply  38060  compneOLD  38961  fmuldfeq  40133  limciccioolb  40171  ditgeq3d  40498  stoweidlem44  40579  dirkertrigeq  40636  fourierdlem32  40674  fourierdlem33  40675  fourierdlem42  40684  fourierdlem62  40703  fourierdlem84  40725  fourierdlem85  40726  fourierdlem97  40738  fourierdlem98  40739  fourierdlem102  40743  fourierdlem104  40745  fourierdlem113  40754  fourierdlem114  40755  fourierswlem  40765  fouriersw  40766  sssalgen  40871  meadjun  40997  deccarry  41646  fsumsplitsndif  41668  funcrngcsetcALT  42324
  Copyright terms: Public domain W3C validator