Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximii | Unicode version |
Description: Inference associated with eximi 1491. (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 1491 | . 2 |
4 | 1, 3 | ax-mp 7 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1381 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: spimed 1628 darii 2000 barbari 2002 festino 2006 baroco 2007 cesaro 2008 camestros 2009 datisi 2010 disamis 2011 felapton 2014 darapti 2015 dimatis 2017 fresison 2018 calemos 2019 fesapo 2020 bamalip 2021 vtoclf 2607 vtocl2 2609 vtocl3 2610 nalset 3887 el 3931 dtruarb 3942 snnex 4181 eusv2nf 4188 limom 4336 bj-axemptylem 10012 bj-nalset 10015 bj-d0clsepcl 10049 bj-omex2 10102 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |