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

Theorem breqtri 4062
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
breqtr.1  |-  A R B
breqtr.2  |-  B  =  C
Assertion
Ref Expression
breqtri  |-  A R C

Proof of Theorem breqtri
StepHypRef Expression
1 breqtr.1 . 2  |-  A R B
2 breqtr.2 . . 3  |-  B  =  C
32breq2i 4047 . 2  |-  ( A R B  <->  A R C )
41, 3mpbi 199 1  |-  A R C
Colors of variables: wff set class
Syntax hints:    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  breqtrri  4064  3brtr3i  4066  supsrlem  8749  0lt1  9312  hashunlei  11393  sqr2gt1lt2  11776  trireciplem  12336  cos1bnd  12483  cos2bnd  12484  cos01gt0  12487  sin4lt0  12491  rpnnen2lem3  12511  gcdaddmlem  12723  dec2dvds  13094  abvtrivd  15621  sincos4thpi  19897  log2cnv  20256  log2ublem2  20259  log2ublem3  20260  birthday  20265  harmonicbnd3  20317  basellem7  20340  ppiublem1  20457  ppiublem2  20458  ppiub  20459  bposlem9  20547  lgsdir2lem2  20579  lgsdir2lem3  20580  ex-fl  20850  siilem1  21445  normlem5  21709  normlem6  21710  norm-ii-i  21732  norm3adifii  21743  cmm2i  22202  mayetes3i  22325  nmopcoadji  22697  mdoc2i  23022  dmdoc2i  23024  ballotlemfc0  23067  ballotlemfcc  23068  sqsscirc1  23307  log2le1  23424  circum  24022  cntotbnd  26623  jm2.23  27192  stoweidlem7  27859  wallispi  27922  stirlinglem1  27926
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator