Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > breq2i | Unicode version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Ref | Expression |
---|---|
breq1i.1 |
Ref | Expression |
---|---|
breq2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 | . 2 | |
2 | breq2 3980 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 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: breqtri 4001 en1 6756 snnen2og 6816 1nen2 6818 pm54.43 7137 caucvgprprlemval 7620 caucvgprprlemmu 7627 caucvgsr 7734 pitonnlem1 7777 lt0neg2 8358 le0neg2 8360 negap0 8519 recexaplem2 8540 recgt1 8783 crap0 8844 addltmul 9084 nn0lt10b 9262 nn0lt2 9263 3halfnz 9279 xlt0neg2 9766 xle0neg2 9768 iccshftr 9921 iccshftl 9923 iccdil 9925 icccntr 9927 fihashen1 10701 cjap0 10835 abs00ap 10990 xrmaxiflemval 11177 mertenslem2 11463 mertensabs 11464 3dvdsdec 11787 3dvds2dec 11788 ndvdsi 11855 3prm 12039 prmfac1 12063 prm23lt5 12174 sinhalfpilem 13259 sincosq1lem 13293 sincosq1sgn 13294 sincosq2sgn 13295 sincosq3sgn 13296 sincosq4sgn 13297 logrpap0b 13344 |
Copyright terms: Public domain | W3C validator |