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

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

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3  |-  B  =  A
21eqcomi 2287 . 2  |-  A  =  B
3 syl5reqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5req 2328 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  bm2.5ii  4597  f1o00  5508  fmpt  5681  fmptsn  5709  mapsn  6809  sbthlem4  6974  sbthlem6  6976  findcard2s  7099  elfiun  7183  cnfcom2  7405  rankxplim3  7551  rankxpsuc  7552  pm54.43  7633  axdc3lem4  8079  gruun  8428  recmulnq  8588  reclem3pr  8673  xrmineq  10509  xadddi2  10617  iooval2  10689  hashsng  11356  hashfun  11389  hashbc  11391  isumclim3  12222  isummulc2  12225  ruclem4  12512  bitsshft  12666  phimullem  12847  pythagtriplem1  12869  1arithlem4  12973  topnid  13340  odhash  14885  gsumzf1o  15196  pgpfaclem1  15316  mplcoe1  16209  mplcoe2  16211  evlslem4  16245  ordtrest2  16934  ufildr  17626  tsmsres  17826  volinun  18903  uniioombllem4  18941  itg1climres  19069  limcco  19243  vieta1lem2  19691  coseq00topi  19870  tangtx  19873  coskpi  19888  advlog  20001  advlogexp  20002  logtayl  20007  logccv  20010  dvcxp1  20082  loglesqr  20098  ang180lem3  20109  dquart  20149  atans2  20227  basellem8  20325  chtub  20451  bposlem6  20528  lgsquadlem2  20594  logdivsum  20682  log2sumbnd  20693  ipval3  21282  siii  21431  cm2j  22199  pjssmii  22260  opsqrlem1  22720  hmopidmchi  22731  hmopidmpji  22732  pjcmul1i  22781  mddmd2  22889  cvexchlem  22948  dmdbr6ati  23003  measxun  23539  cvmlift2lem12  23845  nepss  24072  bpolydiflem  24789  bpoly4  24794  dvreasin  24923  dvreacos  24924  areacirclem2  24925  domcnvpre  25233  vecaddonto  25659  vecscmonto  25686  fninfp  26754  diophrw  26838  wopprc  27123  fsuppeq  27259  glbconN  29566  pmodl42N  30040  2polssN  30104  cdleme20j  30507  trlcocnv  30909  trlcone  30917  lclkrlem2c  31699
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