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

Theorem 3brtr3g 5066
 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 5042 . 2 (𝐴𝑅𝐵𝐶𝑅𝐷)
51, 4sylib 221 1 (𝜑𝐶𝑅𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3887  df-sn 4528  df-pr 4530  df-op 4534  df-br 5034 This theorem is referenced by:  eqbrtrrid  5069  breqtrdi  5074  ssenen  8690  adderpq  10382  mulerpq  10383  ltaddnq  10400  ege2le3  15452  ovolfiniun  24143  dvfsumlem3  24669  basellem9  25715  pnt2  26238  pnt  26239  siilem1  28675  omndaddr  30804  ogrpaddltrd  30816  sn-0ne2  39631
 Copyright terms: Public domain W3C validator