| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > breqtri | GIF version | ||
| Description: Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.) |
| Ref | Expression |
|---|---|
| breqtr.1 | ⊢ 𝐴𝑅𝐵 |
| breqtr.2 | ⊢ 𝐵 = 𝐶 |
| Ref | Expression |
|---|---|
| breqtri | ⊢ 𝐴𝑅𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breqtr.1 | . 2 ⊢ 𝐴𝑅𝐵 | |
| 2 | breqtr.2 | . . 3 ⊢ 𝐵 = 𝐶 | |
| 3 | 2 | breq2i 4052 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶) |
| 4 | 1, 3 | mpbi 145 | 1 ⊢ 𝐴𝑅𝐶 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1373 class class class wbr 4044 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-un 3170 df-sn 3639 df-pr 3640 df-op 3642 df-br 4045 |
| This theorem is referenced by: breqtrri 4071 3brtr3i 4073 le9lt10 9530 9lt10 9634 sqrt2gt1lt2 11360 trireciplem 11811 cos1bnd 12070 cos2bnd 12071 cos01gt0 12074 sin4lt0 12078 z4even 12227 dec2dvds 12734 coseq00topi 15307 sincos4thpi 15312 lgsdir2lem2 15506 lgsdir2lem3 15507 ex-fl 15661 |
| Copyright terms: Public domain | W3C validator |