Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exlimi | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
exlimi.1 | |
exlimi.2 |
Ref | Expression |
---|---|
exlimi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimi.1 | . . 3 | |
2 | 1 | nfri 1452 | . 2 |
3 | exlimi.2 | . 2 | |
4 | 2, 3 | exlimih 1524 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wnf 1389 wex 1421 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-gen 1378 ax-ie2 1423 ax-4 1440 |
This theorem depends on definitions: df-bi 115 df-nf 1390 |
This theorem is referenced by: 19.36i 1602 euexex 2026 ceqsex 2637 sbhypf 2648 vtoclgf 2657 vtoclef 2671 copsexg 3999 copsex2g 4001 ralxpf 4500 rexxpf 4501 dmcoss 4619 fv3 5218 tz6.12c 5224 0neqopab 5570 cnvoprab 5875 bj-exlimmpi 10581 |
Copyright terms: Public domain | W3C validator |