![]() |
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 3908 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbird 166 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-v 2659 df-un 3041 df-sn 3499 df-pr 3500 df-op 3502 df-br 3896 |
This theorem is referenced by: f1oiso2 5682 prarloclemarch2 7175 caucvgprprlemmu 7451 caucvgsrlembound 7536 mulap0 8328 lediv12a 8562 recp1lt1 8567 xleadd1a 9549 fldiv4p1lem1div2 9971 intfracq 9986 modqmulnn 10008 addmodlteq 10064 frecfzennn 10092 monoord2 10143 expgt1 10224 leexp2r 10240 leexp1a 10241 bernneq 10305 faclbnd 10380 faclbnd6 10383 facubnd 10384 hashunlem 10443 zfz1isolemiso 10475 sqrtgt0 10698 absrele 10747 absimle 10748 abstri 10768 abs2difabs 10772 bdtrilem 10902 bdtri 10903 xrmaxifle 10907 xrmaxadd 10922 xrbdtri 10937 climsqz 10996 climsqz2 10997 fsum3cvg2 11055 isumle 11156 expcnvap0 11163 expcnvre 11164 explecnv 11166 cvgratz 11193 efcllemp 11215 ege2le3 11228 eflegeo 11259 phibnd 11738 psmetres2 12322 xmetres2 12368 comet 12488 bdxmet 12490 cnmet 12519 limcimolemlt 12589 cvgcmp2nlemabs 12919 trilpolemlt1 12926 |
Copyright terms: Public domain | W3C validator |