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

Theorem syl6req 2345
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 2344 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2301 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  syl6reqr  2347  somincom  5096  elxp4  5176  elxp5  5177  fo1stres  6159  fo2ndres  6160  eloprabi  6202  opabiotafun  6307  seqomlem2  6479  oev2  6538  odi  6593  fundmen  6950  xpsnen  6962  xpassen  6972  ac6sfi  7117  infeq5  7354  alephsuc3  8218  rankcf  8415  ine0  9231  fzval2  10801  fseq1p1m1  10873  hashfun  11405  hashf1  11411  fsum2dlem  12249  ef4p  12409  sin01bnd  12481  odd2np1  12603  bitsinvp1  12656  smumullem  12699  oppcmon  13657  issubc2  13729  curf1cl  14018  curfcl  14022  cnvtsr  14347  sylow1lem1  14925  sylow2a  14946  pptbas  16761  2ndcctbss  17197  txcmplem1  17351  qtopeu  17423  alexsubALTlem3  17759  xmetdmdm  17916  pcopt  18536  pcorevlem  18540  voliunlem1  18923  i1fima2  19050  iblabs  19199  dveflem  19342  deg1val  19498  abssinper  19902  mulcxplem  20047  dvatan  20247  lgseisenlem1  20604  dchrisumlem1  20654  pntlemr  20767  grporndm  20893  ismgm  21003  ismndo2  21028  vafval  21175  smfval  21177  hvmul0  21619  cmcmlem  22186  cmbr3i  22195  nmbdfnlbi  22645  nmcfnlbi  22648  nmopcoadji  22697  pjin2i  22789  hst1h  22823  xaddeq0  23319  esumcst  23451  dstfrvunirn  23690  subfacp1lem5  23730  cvmliftlem10  23840  ghomfo  24013  ovoliunnfl  25001  itg2addnclem  25003  itg2addnc  25005  iblabsnc  25015  iblmulc2nc  25016  domfldref  25164  cmpltr2  25510  zintdom  25541  domval  25826  codval  25827  idval  25828  cmpval  25829  fnessref  26396  fnemeet2  26419  sdclem2  26555  blbnd  26614  fndifnfp  26859  mzpcompact2lem  26932  diophrw  26941  eldioph2  26944  pellexlem5  27021  pell1qr1  27059  rmxy0  27111  hashtpg  28217  tendo0co2  31599  dvhfvadd  31903  dvh4dimN  32259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator