![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3brtr4i | Structured version Visualization version GIF version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.) |
Ref | Expression |
---|---|
3brtr4.1 | ⊢ 𝐴𝑅𝐵 |
3brtr4.2 | ⊢ 𝐶 = 𝐴 |
3brtr4.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3brtr4i | ⊢ 𝐶𝑅𝐷 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr4.2 | . . 3 ⊢ 𝐶 = 𝐴 | |
2 | 3brtr4.1 | . . 3 ⊢ 𝐴𝑅𝐵 | |
3 | 1, 2 | eqbrtri 5165 | . 2 ⊢ 𝐶𝑅𝐵 |
4 | 3brtr4.3 | . 2 ⊢ 𝐷 = 𝐵 | |
5 | 3, 4 | breqtrri 5171 | 1 ⊢ 𝐶𝑅𝐷 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 class class class wbr 5144 |
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 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5145 |
This theorem is referenced by: 1lt2nq 10955 0lt1sr 11077 declt 12692 decltc 12693 decle 12698 fzennn 13920 faclbnd4lem1 14240 fsumabs 15734 basendxltplusgndx 17213 basendxlttsetndx 17287 basendxltplendx 17301 basendxltdsndx 17320 basendxltunifndx 17330 ovolfiniun 24987 log2ublem3 26420 log2ub 26421 bclbnd 26750 bposlem8 26761 basendxltedgfndx 28220 baseltedgfOLD 28221 nmblolbii 30017 normlem6 30333 norm-ii-i 30355 nmbdoplbi 31242 dp2lt 32022 dp2ltsuc 32023 dp2ltc 32024 dplt 32041 dpltc 32044 dpmul4 32051 hgt750lemd 33591 hgt750lem 33594 supxrltinfxr 44032 nnsum4primesevenALTV 46342 |
Copyright terms: Public domain | W3C validator |