![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3brtr3g | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.) |
Ref | Expression |
---|---|
3brtr3g.1 | ⊢ (𝜑 → 𝐴𝑅𝐵) |
3brtr3g.2 | ⊢ 𝐴 = 𝐶 |
3brtr3g.3 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
3brtr3g | ⊢ (𝜑 → 𝐶𝑅𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr3g.1 | . 2 ⊢ (𝜑 → 𝐴𝑅𝐵) | |
2 | 3brtr3g.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
3 | 3brtr3g.3 | . . 3 ⊢ 𝐵 = 𝐷 | |
4 | 2, 3 | breq12i 5162 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷) |
5 | 1, 4 | sylib 217 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 class class class wbr 5153 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 |
This theorem is referenced by: eqbrtrrid 5189 breqtrdi 5194 ssenen 9189 adderpq 10999 mulerpq 11000 ltaddnq 11017 ege2le3 16092 ovolfiniun 25521 dvfsumlem3 26054 basellem9 27117 pnt2 27642 pnt 27643 siilem1 30784 omndaddr 32942 ogrpaddltrd 32954 sn-0ne2 42186 |
Copyright terms: Public domain | W3C validator |