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

Theorem syl5reqr 2482
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 2439 . 2  |-  A  =  B
3 syl5reqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5req 2480 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  bm2.5ii  4778  f1o00  5702  fmpt  5882  fmptsn  5914  mapsn  7047  sbthlem4  7212  sbthlem6  7214  findcard2s  7341  elfiun  7427  cnfcom2  7649  rankxplim3  7795  rankxpsuc  7796  pm54.43  7877  axdc3lem4  8323  gruun  8671  recmulnq  8831  reclem3pr  8916  xrmineq  10758  xadddi2  10866  iooval2  10939  hashsng  11637  hashfun  11690  hashbc  11692  isumclim3  12533  isummulc2  12536  ruclem4  12823  bitsshft  12977  phimullem  13158  pythagtriplem1  13180  1arithlem4  13284  topnid  13653  odhash  15198  gsumzf1o  15509  pgpfaclem1  15629  mplcoe1  16518  mplcoe2  16520  evlslem4  16554  ordtrest2  17258  ufildr  17953  tsmsres  18163  volinun  19430  uniioombllem4  19468  itg1climres  19596  limcco  19770  vieta1lem2  20218  coseq00topi  20400  tangtx  20403  coskpi  20418  advlog  20535  advlogexp  20536  logtayl  20541  logccv  20544  dvcxp1  20616  loglesqr  20632  ang180lem3  20643  dquart  20683  atans2  20761  basellem8  20860  chtub  20986  bposlem6  21063  lgsquadlem2  21129  logdivsum  21217  log2sumbnd  21228  ipval3  22195  siii  22344  cm2j  23112  pjssmii  23173  opsqrlem1  23633  hmopidmchi  23644  hmopidmpji  23645  pjcmul1i  23694  mddmd2  23802  cvexchlem  23861  dmdbr6ati  23916  difeq  23988  zzsnm  24332  measun  24555  sxbrsigalem2  24626  cvmlift2lem12  24991  nepss  25165  fprodefsum  25288  iprodclim3  25303  bpolydiflem  26065  bpoly4  26070  ismblfin  26210  itg2addnclem3  26221  dvreasin  26243  dvreacos  26244  areacirclem2  26245  fninfp  26689  diophrw  26771  wopprc  27055  fsuppeq  27191  sineq0ALT  28950  glbconN  30075  pmodl42N  30549  2polssN  30613  cdleme20j  31016  trlcocnv  31418  trlcone  31426  lclkrlem2c  32208
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 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator