![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eximii | Unicode version |
Description: Inference associated with eximi 1488. (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 1488 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | ax-mp 7 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: spimed 1625 darii 1997 barbari 1999 festino 2003 baroco 2004 cesaro 2005 camestros 2006 datisi 2007 disamis 2008 felapton 2011 darapti 2012 dimatis 2014 fresison 2015 calemos 2016 fesapo 2017 bamalip 2018 vtoclf 2601 vtocl2 2603 vtocl3 2604 nalset 3878 el 3922 dtruarb 3933 snnex 4147 eusv2nf 4154 limom 4279 bj-axemptylem 9347 bj-nalset 9350 bj-d0clsepcl 9384 bj-omex2 9437 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |