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 3989 | . 2 |
5 | 1, 4 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 class class class wbr 3976 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 df-op 3579 df-br 3977 |
This theorem is referenced by: f1oiso2 5789 prarloclemarch2 7351 caucvgprprlemmu 7627 caucvgsrlembound 7726 mulap0 8542 lediv12a 8780 recp1lt1 8785 xleadd1a 9800 fldiv4p1lem1div2 10230 intfracq 10245 modqmulnn 10267 addmodlteq 10323 frecfzennn 10351 monoord2 10402 expgt1 10483 leexp2r 10499 leexp1a 10500 bernneq 10564 faclbnd 10643 faclbnd6 10646 facubnd 10647 hashunlem 10706 zfz1isolemiso 10738 sqrtgt0 10962 absrele 11011 absimle 11012 abstri 11032 abs2difabs 11036 bdtrilem 11166 bdtri 11167 xrmaxifle 11173 xrmaxadd 11188 xrbdtri 11203 climsqz 11262 climsqz2 11263 fsum3cvg2 11321 isumle 11422 expcnvap0 11429 expcnvre 11430 explecnv 11432 cvgratz 11459 efcllemp 11585 ege2le3 11598 eflegeo 11628 cos12dec 11694 phibnd 12128 pcdvdstr 12237 pcprmpw2 12243 pockthg 12266 psmetres2 12880 xmetres2 12926 comet 13046 bdxmet 13048 cnmet 13077 ivthdec 13169 limcimolemlt 13180 tangtx 13306 logbgcd1irraplemap 13434 cvgcmp2nlemabs 13752 trilpolemlt1 13761 |
Copyright terms: Public domain | W3C validator |