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

Theorem syl6req 2485
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6req.1  |-  ( ph  ->  A  =  B )
syl6req.2  |-  B  =  C
Assertion
Ref Expression
syl6req  |-  ( ph  ->  C  =  A )

Proof of Theorem syl6req
StepHypRef Expression
1 syl6req.1 . . 3  |-  ( ph  ->  A  =  B )
2 syl6req.2 . . 3  |-  B  =  C
31, 2syl6eq 2484 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2441 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  syl6reqr  2487  somincom  5271  elxp4  5357  elxp5  5358  fo1stres  6370  fo2ndres  6371  eloprabi  6413  fo2ndf  6453  opabiotafun  6536  seqomlem2  6708  oev2  6767  odi  6822  fundmen  7180  xpsnen  7192  xpassen  7202  ac6sfi  7351  infeq5  7592  alephsuc3  8455  rankcf  8652  ine0  9469  nn0n0n1ge2  10280  fzval2  11046  fseq1p1m1  11122  hashtpg  11691  hashfun  11700  hashf1  11706  fsum2dlem  12554  ef4p  12714  sin01bnd  12786  odd2np1  12908  bitsinvp1  12961  smumullem  13004  oppcmon  13964  issubc2  14036  curf1cl  14325  curfcl  14329  cnvtsr  14654  sylow1lem1  15232  sylow2a  15253  pptbas  17072  2ndcctbss  17518  txcmplem1  17673  qtopeu  17748  alexsubALTlem3  18080  ustuqtop5  18275  psmetdmdm  18336  xmetdmdm  18365  pcopt  19047  pcorevlem  19051  voliunlem1  19444  i1fima2  19571  iblabs  19720  dveflem  19863  deg1val  20019  abssinper  20426  mulcxplem  20575  dvatan  20775  lgseisenlem1  21133  dchrisumlem1  21183  pntlemr  21296  grporndm  21798  ismgm  21908  ismndo2  21933  vafval  22082  smfval  22084  hvmul0  22526  cmcmlem  23093  cmbr3i  23102  nmbdfnlbi  23552  nmcfnlbi  23555  nmopcoadji  23604  pjin2i  23696  hst1h  23730  xaddeq0  24119  esumcst  24455  dstfrvunirn  24732  lgamgulmlem2  24814  lgamgulmlem5  24817  subfacp1lem5  24870  cvmliftlem10  24981  ghomfo  25102  fprod2dlem  25304  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  itg2addnclem  26256  itg2addnc  26259  iblabsnc  26269  iblmulc2nc  26270  ftc1anclem2  26281  fnessref  26373  fnemeet2  26396  sdclem2  26446  blbnd  26496  fndifnfp  26737  mzpcompact2lem  26808  diophrw  26817  eldioph2  26820  pellexlem5  26896  pell1qr1  26934  rmxy0  26986  usgra2wlkspthlem1  28306  tendo0co2  31585  dvhfvadd  31889  dvh4dimN  32245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator