![]() |
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 4015 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbird 167 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-un 3133 df-sn 3598 df-pr 3599 df-op 3601 df-br 4003 |
This theorem is referenced by: f1oiso2 5825 prarloclemarch2 7415 caucvgprprlemmu 7691 caucvgsrlembound 7790 mulap0 8607 lediv12a 8847 recp1lt1 8852 xleadd1a 9869 fldiv4p1lem1div2 10300 intfracq 10315 modqmulnn 10337 addmodlteq 10393 frecfzennn 10421 monoord2 10472 expgt1 10553 leexp2r 10569 leexp1a 10570 bernneq 10635 faclbnd 10714 faclbnd6 10717 facubnd 10718 hashunlem 10777 zfz1isolemiso 10812 sqrtgt0 11036 absrele 11085 absimle 11086 abstri 11106 abs2difabs 11110 bdtrilem 11240 bdtri 11241 xrmaxifle 11247 xrmaxadd 11262 xrbdtri 11277 climsqz 11336 climsqz2 11337 fsum3cvg2 11395 isumle 11496 expcnvap0 11503 expcnvre 11504 explecnv 11506 cvgratz 11533 efcllemp 11659 ege2le3 11672 eflegeo 11702 cos12dec 11768 phibnd 12209 pcdvdstr 12318 pcprmpw2 12324 pockthg 12347 psmetres2 13704 xmetres2 13750 comet 13870 bdxmet 13872 cnmet 13901 ivthdec 13993 limcimolemlt 14004 tangtx 14130 logbgcd1irraplemap 14258 cvgcmp2nlemabs 14640 trilpolemlt1 14649 |
Copyright terms: Public domain | W3C validator |