| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > elind | Unicode version | ||
| Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
| Ref | Expression |
|---|---|
| elind.1 |
|
| elind.2 |
|
| Ref | Expression |
|---|---|
| elind |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elind.1 |
. 2
| |
| 2 | elind.2 |
. 2
| |
| 3 | elin 3390 |
. 2
| |
| 4 | 1, 2, 3 | sylanbrc 417 |
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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-v 2804 df-in 3206 |
| This theorem is referenced by: fnfvimad 5890 elfir 7172 infpwfidom 7409 nninfdclemcl 13087 nninfdclemp1 13089 strslfv2d 13143 bassetsnn 13157 insubm 13586 2idl0 14545 2idl1 14546 baspartn 14793 bastg 14804 isopn3 14868 restbasg 14911 lmss 14989 metrest 15249 tgioo 15297 dvmulxxbr 15445 elply2 15478 pilem3 15526 2sqlem7 15869 |
| Copyright terms: Public domain | W3C validator |