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

Theorem syl5reqr 2343
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 2300 . 2  |-  A  =  B
3 syl5reqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5req 2341 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  bm2.5ii  4613  f1o00  5524  fmpt  5697  fmptsn  5725  mapsn  6825  sbthlem4  6990  sbthlem6  6992  findcard2s  7115  elfiun  7199  cnfcom2  7421  rankxplim3  7567  rankxpsuc  7568  pm54.43  7649  axdc3lem4  8095  gruun  8444  recmulnq  8604  reclem3pr  8689  xrmineq  10525  xadddi2  10633  iooval2  10705  hashsng  11372  hashfun  11405  hashbc  11407  isumclim3  12238  isummulc2  12241  ruclem4  12528  bitsshft  12682  phimullem  12863  pythagtriplem1  12885  1arithlem4  12989  topnid  13356  odhash  14901  gsumzf1o  15212  pgpfaclem1  15332  mplcoe1  16225  mplcoe2  16227  evlslem4  16261  ordtrest2  16950  ufildr  17642  tsmsres  17842  volinun  18919  uniioombllem4  18957  itg1climres  19085  limcco  19259  vieta1lem2  19707  coseq00topi  19886  tangtx  19889  coskpi  19904  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  loglesqr  20114  ang180lem3  20125  dquart  20165  atans2  20243  basellem8  20341  chtub  20467  bposlem6  20544  lgsquadlem2  20610  logdivsum  20698  log2sumbnd  20709  ipval3  21298  siii  21447  cm2j  22215  pjssmii  22276  opsqrlem1  22736  hmopidmchi  22747  hmopidmpji  22748  pjcmul1i  22797  mddmd2  22905  cvexchlem  22964  dmdbr6ati  23019  measxun  23554  cvmlift2lem12  23860  nepss  24087  bpolydiflem  24861  bpoly4  24866  itg2addnc  25005  dvreasin  25026  dvreacos  25027  areacirclem2  25028  domcnvpre  25336  vecaddonto  25762  vecscmonto  25789  fninfp  26857  diophrw  26941  wopprc  27226  fsuppeq  27362  glbconN  30188  pmodl42N  30662  2polssN  30726  cdleme20j  31129  trlcocnv  31531  trlcone  31539  lclkrlem2c  32321
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