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

Theorem 3brtr4g 4474
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
Hypotheses
Ref Expression
3brtr4g.1  |-  ( ph  ->  A R B )
3brtr4g.2  |-  C  =  A
3brtr4g.3  |-  D  =  B
Assertion
Ref Expression
3brtr4g  |-  ( ph  ->  C R D )

Proof of Theorem 3brtr4g
StepHypRef Expression
1 3brtr4g.1 . 2  |-  ( ph  ->  A R B )
2 3brtr4g.2 . . 3  |-  C  =  A
3 3brtr4g.3 . . 3  |-  D  =  B
42, 3breq12i 4451 . 2  |-  ( C R D  <->  A R B )
51, 4sylibr 212 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374   class class class wbr 4442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443
This theorem is referenced by:  syl5eqbr  4475  limensuci  7685  infensuc  7687  rlimneg  13420  isumsup2  13612  crt  14158  4sqlem6  14311  gzrngunit  18246  matgsum  18701  ovolunlem1a  21637  ovolfiniun  21642  ioombl1lem1  21698  ioombl1lem4  21701  iblss  21941  itgle  21946  dvfsumlem3  22159  emcllem6  23053  pntpbnd1a  23493  ostth2lem4  23544  omsmon  27895  itg2gt0cn  29636  dalem-cly  34344  dalem10  34346
  Copyright terms: Public domain W3C validator