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 1825 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | eximi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1789 | 1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 2eximi 1827 eximii 1828 exa1 1829 exsimpl 1860 exsimpr 1861 19.29r2 1867 19.29x 1868 19.35 1869 19.40-2 1879 emptyex 1899 exlimiv 1922 speimfwALT 1958 spsbeOLD 2080 19.12 2337 ax13lem2 2385 exdistrf 2461 equs45f 2474 sbimiOLD 2508 sbimiALT 2570 dfmoeu 2611 moimi 2620 eu6 2652 2eu2ex 2721 reximi2 3241 cgsexg 3535 gencbvex 3547 eqvincg 3638 n0rex 4311 axrep2 5184 bm1.3ii 5197 ax6vsep 5198 copsexgw 5372 copsexg 5373 relopabi 5687 dminss 6003 imainss 6004 iotaex 6328 fv3 6681 ssimaex 6741 dffv2 6749 exfo 6863 oprabidw 7176 oprabid 7177 zfrep6 7645 frxp 7809 suppimacnvss 7829 tz7.48-1 8068 enssdom 8522 fineqvlem 8720 infcntss 8780 infeq5 9088 omex 9094 rankuni 9280 scott0 9303 acni3 9461 acnnum 9466 dfac3 9535 dfac9 9550 kmlem1 9564 cflm 9660 cfcof 9684 axdc4lem 9865 axcclem 9867 ac6c4 9891 ac6s 9894 ac6s2 9896 axdclem2 9930 brdom3 9938 brdom5 9939 brdom4 9940 nqpr 10424 ltexprlem4 10449 reclem2pr 10458 hash1to3 13837 trclublem 14343 fnpr2ob 16819 drsdirfi 17536 toprntopon 21461 2ndcsb 21985 fbssint 22374 isfil2 22392 alexsubALTlem3 22585 lpbl 23040 metustfbas 23094 ex-natded9.26-2 28126 19.9d2rf 30162 rexunirn 30183 f1ocnt 30451 fsumiunle 30472 fmcncfil 31073 esumiun 31252 0elsiga 31272 ddemeas 31394 bnj168 31899 bnj593 31915 bnj607 32087 bnj600 32090 bnj916 32104 lfuhgr3 32263 cusgredgex 32265 loop1cycl 32281 umgr2cycl 32285 fundmpss 32906 exisym1 33669 bj-sylge 33854 bj-19.12 33987 bj-equs45fv 34030 bj-snsetex 34172 bj-snglss 34179 bj-snglex 34182 bj-bm1.3ii 34251 bj-restn0 34275 bj-ccinftydisj 34387 mptsnunlem 34501 pibt2 34580 wl-cbvmotv 34635 wl-moae 34638 wl-nax6im 34640 iscard4 39778 spsbce-2 40590 iotaexeu 40627 iotasbc 40628 relopabVD 41112 ax6e2ndeqVD 41120 2uasbanhVD 41122 ax6e2ndeqALT 41142 fnchoice 41163 rfcnnnub 41170 stoweidlem35 42197 stoweidlem57 42219 |
Copyright terms: Public domain | W3C validator |