![]() |
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 1550 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | excomim 1550 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 117 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: excom13 1576 exrot3 1577 ee4anv 1806 sbexyz 1876 2exsb 1882 2euex 1984 2exeu 1989 2eu4 1990 rexcomf 2466 gencbvex 2594 euxfr2dc 2720 euind 2722 sbccomlem 2826 opelopabsbALT 3987 uniuni 4149 elvvv 4346 dmuni 4488 dm0rn0 4495 dmmrnm 4497 dmcosseq 4546 elres 4589 rnco 4770 coass 4782 oprabid 5480 dfoprab2 5494 opabex3d 5690 opabex3 5691 domen 6168 xpassen 6240 prarloc 6486 |
Copyright terms: Public domain | W3C validator |