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

Theorem 3brtr4g 4647
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
Hypotheses
Ref Expression
3brtr4g.1 (𝜑𝐴𝑅𝐵)
3brtr4g.2 𝐶 = 𝐴
3brtr4g.3 𝐷 = 𝐵
Assertion
Ref Expression
3brtr4g (𝜑𝐶𝑅𝐷)

Proof of Theorem 3brtr4g
StepHypRef Expression
1 3brtr4g.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr4g.2 . . 3 𝐶 = 𝐴
3 3brtr4g.3 . . 3 𝐷 = 𝐵
42, 3breq12i 4622 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 224 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480   class class class wbr 4613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614
This theorem is referenced by:  syl5eqbr  4648  limensuci  8080  infensuc  8082  rlimneg  14311  isumsup2  14503  crth  15407  4sqlem6  15571  gzrngunit  19731  matgsum  20162  ovolunlem1a  23171  ovolfiniun  23176  ioombl1lem1  23233  ioombl1lem4  23236  iblss  23477  itgle  23482  dvfsumlem3  23695  emcllem6  24627  gausslemma2dlem0f  24986  gausslemma2dlem0g  24987  pntpbnd1a  25174  ostth2lem4  25225  omsmon  30141  itg2gt0cn  33097  dalem-cly  34437  dalem10  34439  fourierdlem103  39733  fourierdlem104  39734
  Copyright terms: Public domain W3C validator