Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximi | Unicode version |
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eximi.1 |
Ref | Expression |
---|---|
eximi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1586 | . 2 | |
2 | eximi.1 | . 2 | |
3 | 1, 2 | mpg 1438 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1479 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-ial 1521 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2eximi 1588 eximii 1589 exsimpl 1604 exsimpr 1605 19.29r2 1609 19.29x 1610 19.35-1 1611 19.43 1615 19.40 1618 19.40-2 1619 exanaliim 1634 19.12 1652 equs4 1712 cbvexh 1742 equvini 1745 sbimi 1751 equs5e 1782 exdistrfor 1787 equs45f 1789 sbcof2 1797 sbequi 1826 spsbe 1829 sbidm 1838 cbvexdh 1913 eumo0 2044 mor 2055 euan 2069 eupickb 2094 2eu2ex 2102 2exeu 2105 rexex 2510 reximi2 2560 cgsexg 2756 gencbvex 2767 gencbval 2769 vtocl3 2777 eqvinc 2844 eqvincg 2845 mosubt 2898 rexm 3503 prmg 3691 bm1.3ii 4097 a9evsep 4098 axnul 4101 dminss 5012 imainss 5013 euiotaex 5163 imadiflem 5261 funimaexglem 5265 brprcneu 5473 fv3 5503 relelfvdm 5512 ssimaex 5541 oprabid 5865 brabvv 5879 ecexr 6497 enssdom 6719 fidcenumlemim 6908 subhalfnqq 7346 prarloc 7435 ltexprlemopl 7533 ltexprlemlol 7534 ltexprlemopu 7535 ltexprlemupu 7536 bdbm1.3ii 13614 bj-inex 13630 bj-2inf 13661 |
Copyright terms: Public domain | W3C validator |