Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3brtr4d | Unicode version |
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.) |
Ref | Expression |
---|---|
3brtr4d.1 | |
3brtr4d.2 | |
3brtr4d.3 |
Ref | Expression |
---|---|
3brtr4d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3brtr4d.1 | . 2 | |
2 | 3brtr4d.2 | . . 3 | |
3 | 3brtr4d.3 | . . 3 | |
4 | 2, 3 | breq12d 3942 | . 2 |
5 | 1, 4 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 class class class wbr 3929 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 df-br 3930 |
This theorem is referenced by: f1oiso2 5728 prarloclemarch2 7227 caucvgprprlemmu 7503 caucvgsrlembound 7602 mulap0 8415 lediv12a 8652 recp1lt1 8657 xleadd1a 9656 fldiv4p1lem1div2 10078 intfracq 10093 modqmulnn 10115 addmodlteq 10171 frecfzennn 10199 monoord2 10250 expgt1 10331 leexp2r 10347 leexp1a 10348 bernneq 10412 faclbnd 10487 faclbnd6 10490 facubnd 10491 hashunlem 10550 zfz1isolemiso 10582 sqrtgt0 10806 absrele 10855 absimle 10856 abstri 10876 abs2difabs 10880 bdtrilem 11010 bdtri 11011 xrmaxifle 11015 xrmaxadd 11030 xrbdtri 11045 climsqz 11104 climsqz2 11105 fsum3cvg2 11163 isumle 11264 expcnvap0 11271 expcnvre 11272 explecnv 11274 cvgratz 11301 efcllemp 11364 ege2le3 11377 eflegeo 11408 cos12dec 11474 phibnd 11893 psmetres2 12502 xmetres2 12548 comet 12668 bdxmet 12670 cnmet 12699 ivthdec 12791 limcimolemlt 12802 tangtx 12919 cvgcmp2nlemabs 13227 trilpolemlt1 13234 |
Copyright terms: Public domain | W3C validator |