New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 1575 | . 2 | |
2 | eximi.1 | . 2 | |
3 | 1, 2 | mpg 1548 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wex 1541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: 2eximi 1577 exsimpl 1592 19.29r2 1598 19.29x 1599 19.40 1609 19.40-2 1610 exlimiv 1634 speimfw 1645 sbimi 1652 exiftru 1657 spimeh 1667 equid 1676 exlimivOLD 1698 19.12 1847 19.12OLD 1848 cbv3hv 1850 equs4 1959 exdistrf 1971 equvini 1987 equs45f 1989 sbequi 2059 eumo0 2228 euan 2261 eupickb 2269 2eu2ex 2278 darii 2303 barbari 2305 festino 2309 baroco 2310 cesaro 2311 camestros 2312 datisi 2313 disamis 2314 felapton 2317 darapti 2318 dimatis 2320 fresison 2321 calemos 2322 fesapo 2323 bamalip 2324 rexex 2673 reximi2 2720 cgsexg 2890 gencbvex 2901 vtoclf 2908 vtocl3 2911 eqvinc 2966 iotaex 4356 phiall 4618 dmcoss 4971 imassrn 5009 dminss 5041 imainss 5042 fv3 5341 oprabid 5550 nenpw1pwlem2 6085 ncelncs 6120 lecidg 6196 lec0cg 6198 lecncvg 6199 addlec 6208 te0c 6237 dmfrec 6316 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |