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

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

Proof of Theorem 3brtr4i
StepHypRef Expression
1 3brtr4.2 . . 3  |-  C  =  A
2 3brtr4.1 . . 3  |-  A R B
31, 2eqbrtri 4452 . 2  |-  C R B
4 3brtr4.3 . 2  |-  D  =  B
53, 4breqtrri 4458 1  |-  C R D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381   class class class wbr 4433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434
This theorem is referenced by:  1lt2nq  9349  0lt1sr  9470  declt  11000  decltc  11001  fzennn  12052  faclbnd4lem1  12345  fsumabs  13589  ovolfiniun  21778  log2ublem3  23144  log2ub  23145  emgt0  23201  bclbnd  23420  bposlem8  23431  nmblolbii  25579  normlem6  25897  norm-ii-i  25919  nmbdoplbi  26808
  Copyright terms: Public domain W3C validator