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

Theorem syl6req 2332
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 2331 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2288 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  syl6reqr  2334  somincom  5080  elxp4  5160  elxp5  5161  fo1stres  6143  fo2ndres  6144  eloprabi  6186  opabiotafun  6291  seqomlem2  6463  oev2  6522  odi  6577  fundmen  6934  xpsnen  6946  xpassen  6956  ac6sfi  7101  infeq5  7338  alephsuc3  8202  rankcf  8399  ine0  9215  fzval2  10785  fseq1p1m1  10857  hashfun  11389  hashf1  11395  fsum2dlem  12233  ef4p  12393  sin01bnd  12465  odd2np1  12587  bitsinvp1  12640  smumullem  12683  oppcmon  13641  issubc2  13713  curf1cl  14002  curfcl  14006  cnvtsr  14331  sylow1lem1  14909  sylow2a  14930  pptbas  16745  2ndcctbss  17181  txcmplem1  17335  qtopeu  17407  alexsubALTlem3  17743  xmetdmdm  17900  pcopt  18520  pcorevlem  18524  voliunlem1  18907  i1fima2  19034  iblabs  19183  dveflem  19326  deg1val  19482  abssinper  19886  mulcxplem  20031  dvatan  20231  lgseisenlem1  20588  dchrisumlem1  20638  pntlemr  20751  grporndm  20877  ismgm  20987  ismndo2  21012  vafval  21159  smfval  21161  hvmul0  21603  cmcmlem  22170  cmbr3i  22179  nmbdfnlbi  22629  nmcfnlbi  22632  nmopcoadji  22681  pjin2i  22773  hst1h  22807  xaddeq0  23304  esumcst  23436  dstfrvunirn  23675  subfacp1lem5  23715  cvmliftlem10  23825  ghomfo  23998  domfldref  25061  cmpltr2  25407  zintdom  25438  domval  25723  codval  25724  idval  25725  cmpval  25726  fnessref  26293  fnemeet2  26316  sdclem2  26452  blbnd  26511  fndifnfp  26756  mzpcompact2lem  26829  diophrw  26838  eldioph2  26841  pellexlem5  26918  pell1qr1  26956  rmxy0  27008  tendo0co2  30977  dvhfvadd  31281  dvh4dimN  31637
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator