![]() |
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 1622 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | excomim 1622 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 125 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-ial 1495 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: excom13 1648 exrot3 1649 ee4anv 1882 sbexyz 1952 2exsb 1958 2euex 2060 2exeu 2065 2eu4 2066 rexcomf 2565 gencbvex 2701 euxfr2dc 2836 euind 2838 sbccomlem 2949 opelopabsbALT 4139 uniuni 4330 elvvv 4560 elco 4663 dmuni 4707 dm0rn0 4714 dmmrnm 4716 dmcosseq 4766 elres 4811 rnco 5001 coass 5013 oprabid 5755 dfoprab2 5770 opabex3d 5971 opabex3 5972 cnvoprab 6083 domen 6597 xpassen 6675 prarloc 7253 fisumcom2 11093 |
Copyright terms: Public domain | W3C validator |