![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqsstrid | Unicode version |
Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
eqsstrid.1 |
![]() ![]() ![]() ![]() |
eqsstrid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqsstrid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstrid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqsstrid.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | sseq1i 3181 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylibr 134 |
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-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 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-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: eqsstrrid 3202 inss 3365 difsnss 3737 tpssi 3757 peano5 4594 xpsspw 4735 iotanul 5189 iotass 5191 fun 5384 fun11iun 5478 fvss 5525 fmpt 5662 fliftrel 5787 opabbrex 5913 1stcof 6158 2ndcof 6159 tfrlemibacc 6321 tfrlemibfn 6323 tfr1onlemssrecs 6334 tfr1onlembacc 6337 tfr1onlembfn 6339 tfrcllemssrecs 6347 tfrcllembacc 6350 tfrcllembfn 6352 caucvgprlemladdrl 7665 peano5nnnn 7879 peano5nni 8908 un0addcl 9195 un0mulcl 9196 strleund 12541 mgmidsssn0 12692 cnptopco 13382 cnconst2 13393 xmetresbl 13600 blsscls2 13653 bj-omtrans 14357 |
Copyright terms: Public domain | W3C validator |