![]() |
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 5112 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷) |
5 | 1, 4 | sylib 217 | 1 ⊢ (𝜑 → 𝐶𝑅𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 class class class wbr 5103 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 |
This theorem is referenced by: eqbrtrrid 5139 breqtrdi 5144 ssenen 9091 adderpq 10888 mulerpq 10889 ltaddnq 10906 ege2le3 15964 ovolfiniun 24849 dvfsumlem3 25376 basellem9 26422 pnt2 26945 pnt 26946 siilem1 29679 omndaddr 31798 ogrpaddltrd 31810 sn-0ne2 40813 |
Copyright terms: Public domain | W3C validator |