Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximii | Unicode version |
Description: Inference associated with eximi 1531. (Contributed by BJ, 3-Feb-2018.) |
Ref | Expression |
---|---|
eximii.1 | |
eximii.2 |
Ref | Expression |
---|---|
eximii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximii.1 | . 2 | |
2 | eximii.2 | . . 3 | |
3 | 2 | eximi 1531 | . 2 |
4 | 1, 3 | ax-mp 7 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1421 |
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 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: spimed 1668 darii 2041 barbari 2043 festino 2047 baroco 2048 cesaro 2049 camestros 2050 datisi 2051 disamis 2052 felapton 2055 darapti 2056 dimatis 2058 fresison 2059 calemos 2060 fesapo 2061 bamalip 2062 vtoclf 2652 vtocl2 2654 vtocl3 2655 nalset 3908 el 3952 dtruarb 3962 snnex 4199 eusv2nf 4206 dtruex 4302 limom 4354 bj-axemptylem 10683 bj-nalset 10686 bj-d0clsepcl 10720 bj-omex2 10772 bj-nn0sucALT 10773 |
Copyright terms: Public domain | W3C validator |