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

Theorem 3brtr3i 4131
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
Hypotheses
Ref Expression
3brtr3.1  |-  A R B
3brtr3.2  |-  A  =  C
3brtr3.3  |-  B  =  D
Assertion
Ref Expression
3brtr3i  |-  C R D

Proof of Theorem 3brtr3i
StepHypRef Expression
1 3brtr3.2 . . 3  |-  A  =  C
2 3brtr3.1 . . 3  |-  A R B
31, 2eqbrtrri 4125 . 2  |-  C R B
4 3brtr3.3 . 2  |-  B  =  D
53, 4breqtri 4127 1  |-  C R D
Colors of variables: wff set class
Syntax hints:    = wceq 1642   class class class wbr 4104
This theorem is referenced by:  supsrlem  8823  ef01bndlem  12561  pige3  19992  log2ublem1  20353  log2ub  20356  ppiublem1  20553  logfacrlim2  20577  chebbnd1  20733  nmoptri2i  22793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105
  Copyright terms: Public domain W3C validator