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

Theorem 3brtr4g 4830
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 4805 . 2 (𝐶𝑅𝐷𝐴𝑅𝐵)
51, 4sylibr 224 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624   class class class wbr 4796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797
This theorem is referenced by:  syl5eqbr  4831  limensuci  8293  infensuc  8295  rlimneg  14568  isumsup2  14769  crth  15677  4sqlem6  15841  gzrngunit  20006  matgsum  20437  ovolunlem1a  23456  ovolfiniun  23461  ioombl1lem1  23518  ioombl1lem4  23521  iblss  23762  itgle  23767  dvfsumlem3  23982  emcllem6  24918  gausslemma2dlem0f  25277  gausslemma2dlem0g  25278  pntpbnd1a  25465  ostth2lem4  25516  omsmon  30661  itg2gt0cn  33770  dalem-cly  35452  dalem10  35454  fourierdlem103  40921  fourierdlem104  40922
  Copyright terms: Public domain W3C validator