Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximi | GIF 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 1578 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | eximi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1427 | 1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1468 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2eximi 1580 eximii 1581 exsimpl 1596 exsimpr 1597 19.29r2 1601 19.29x 1602 19.35-1 1603 19.43 1607 19.40 1610 19.40-2 1611 exanaliim 1626 19.12 1643 equs4 1703 cbvexh 1728 equvini 1731 sbimi 1737 equs5e 1767 exdistrfor 1772 equs45f 1774 sbcof2 1782 sbequi 1811 spsbe 1814 sbidm 1823 cbvexdh 1898 eumo0 2030 mor 2041 euan 2055 eupickb 2080 2eu2ex 2088 2exeu 2091 rexex 2479 reximi2 2528 cgsexg 2721 gencbvex 2732 gencbval 2734 vtocl3 2742 eqvinc 2808 eqvincg 2809 mosubt 2861 rexm 3462 prmg 3644 bm1.3ii 4049 a9evsep 4050 axnul 4053 dminss 4953 imainss 4954 euiotaex 5104 imadiflem 5202 funimaexglem 5206 brprcneu 5414 fv3 5444 relelfvdm 5453 ssimaex 5482 oprabid 5803 brabvv 5817 ecexr 6434 enssdom 6656 fidcenumlemim 6840 subhalfnqq 7229 prarloc 7318 ltexprlemopl 7416 ltexprlemlol 7417 ltexprlemopu 7418 ltexprlemupu 7419 bdbm1.3ii 13099 bj-inex 13115 bj-2inf 13146 |
Copyright terms: Public domain | W3C validator |