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 1626 | . 2 | |
2 | excomim 1626 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wex 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: excom13 1652 exrot3 1653 ee4anv 1886 sbexyz 1956 2exsb 1962 2euex 2064 2exeu 2069 2eu4 2070 rexcomf 2570 gencbvex 2706 euxfr2dc 2842 euind 2844 sbccomlem 2955 opelopabsbALT 4151 uniuni 4342 elvvv 4572 elco 4675 dmuni 4719 dm0rn0 4726 dmmrnm 4728 dmcosseq 4780 elres 4825 rnco 5015 coass 5027 oprabid 5771 dfoprab2 5786 opabex3d 5987 opabex3 5988 cnvoprab 6099 domen 6613 xpassen 6692 prarloc 7279 fisumcom2 11175 |
Copyright terms: Public domain | W3C validator |