![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eximi | Structured version Visualization version GIF version |
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.) |
Ref | Expression |
---|---|
eximi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
eximi | ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim 1801 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | eximi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1764 | 1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1744 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 |
This theorem depends on definitions: df-bi 197 df-ex 1745 |
This theorem is referenced by: 2eximi 1803 eximii 1804 exa1 1805 exan 1828 exsimpl 1835 exsimpr 1836 19.29r2 1843 19.29x 1844 19.35 1845 19.40-2 1854 exlimiv 1898 speimfwALT 1934 sbimi 1943 19.12 2200 ax13lem2 2332 exdistrf 2364 equs45f 2378 mo2v 2505 2eu2ex 2575 reximi2 3039 cgsexg 3269 gencbvex 3281 vtocl3 3293 eqvincg 3360 n0rex 3968 axrep2 4806 bm1.3ii 4817 ax6vsep 4818 copsexg 4985 relopabi 5278 dminss 5582 imainss 5583 elsnxpOLD 5716 iotaex 5906 fv3 6244 ssimaex 6302 dffv2 6310 exfo 6417 oprabid 6717 zfrep6 7176 frxp 7332 suppimacnvss 7350 tz7.48-1 7583 enssdom 8022 fineqvlem 8215 infcntss 8275 infeq5 8572 omex 8578 rankuni 8764 scott0 8787 acni3 8908 acnnum 8913 dfac3 8982 dfac9 8996 kmlem1 9010 cflm 9110 cfcof 9134 axdc4lem 9315 axcclem 9317 ac6c4 9341 ac6s 9344 ac6s2 9346 axdclem2 9380 brdom3 9388 brdom5 9389 brdom4 9390 nqpr 9874 ltexprlem4 9899 reclem2pr 9908 hash1to3 13311 trclublem 13780 drsdirfi 16985 toprntopon 20777 2ndcsb 21300 fbssint 21689 isfil2 21707 alexsubALTlem3 21900 lpbl 22355 metustfbas 22409 ex-natded9.26-2 27407 19.9d2rf 29446 rexunirn 29458 f1ocnt 29687 fsumiunle 29703 fmcncfil 30105 esumiun 30284 0elsiga 30305 ddemeas 30427 bnj168 30924 bnj593 30941 bnj607 31112 bnj600 31115 bnj916 31129 fundmpss 31790 exisym1 32548 bj-exlime 32734 bj-sbex 32751 bj-ssbequ2 32768 bj-equs45fv 32877 bj-axrep2 32914 bj-eumo0 32955 bj-snsetex 33076 bj-snglss 33083 bj-snglex 33086 bj-restn0 33168 bj-ccinftydisj 33230 mptsnunlem 33315 spsbce-2 38897 iotaexeu 38936 iotasbc 38937 relopabVD 39451 ax6e2ndeqVD 39459 2uasbanhVD 39461 ax6e2ndeqALT 39481 fnchoice 39502 rfcnnnub 39509 stoweidlem35 40570 stoweidlem57 40592 |
Copyright terms: Public domain | W3C validator |