![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > excom | Unicode version |
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
excom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | excomim 1598 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | excomim 1598 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 124 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: excom13 1624 exrot3 1625 ee4anv 1857 sbexyz 1927 2exsb 1933 2euex 2035 2exeu 2040 2eu4 2041 rexcomf 2529 gencbvex 2665 euxfr2dc 2800 euind 2802 sbccomlem 2913 opelopabsbALT 4084 uniuni 4271 elvvv 4497 elco 4598 dmuni 4642 dm0rn0 4649 dmmrnm 4651 dmcosseq 4700 elres 4743 rnco 4932 coass 4944 oprabid 5673 dfoprab2 5688 opabex3d 5884 opabex3 5885 cnvoprab 5991 domen 6458 xpassen 6536 prarloc 7052 fisumcom2 10819 |
Copyright terms: Public domain | W3C validator |