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

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

Proof of Theorem 3brtr3g
StepHypRef Expression
1 3brtr3g.1 . 2 (𝜑𝐴𝑅𝐵)
2 3brtr3g.2 . . 3 𝐴 = 𝐶
3 3brtr3g.3 . . 3 𝐵 = 𝐷
42, 3breq12i 5158 . 2 (𝐴𝑅𝐵𝐶𝑅𝐷)
51, 4sylib 217 1 (𝜑𝐶𝑅𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150
This theorem is referenced by:  eqbrtrrid  5185  breqtrdi  5190  ssenen  9151  adderpq  10951  mulerpq  10952  ltaddnq  10969  ege2le3  16033  ovolfiniun  25018  dvfsumlem3  25545  basellem9  26593  pnt2  27116  pnt  27117  siilem1  30104  omndaddr  32225  ogrpaddltrd  32237  sn-0ne2  41279
  Copyright terms: Public domain W3C validator