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 1836 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | eximi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1800 | 1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 2eximi 1838 eximii 1839 exa1 1840 exsimpl 1871 exsimpr 1872 19.29r2 1878 19.29x 1879 19.35 1880 19.40-2 1890 emptyex 1910 exlimiv 1933 speimfwALT 1968 19.12 2321 ax13lem2 2376 exdistrf 2447 equs45f 2459 dfmoeu 2536 moimi 2545 eu6 2574 2eu2ex 2645 reximi2 3175 cgsexg 3474 gencbvex 3488 eqvincg 3578 sbcg 3795 n0rex 4288 axrep2 5212 bm1.3ii 5226 ax6vsep 5227 copsexgw 5404 copsexg 5405 relopabi 5732 dminss 6056 imainss 6057 iotaex 6413 fv3 6792 ssimaex 6853 dffv2 6863 exfo 6981 oprabidw 7306 oprabid 7307 zfrep6 7797 frxp 7967 suppimacnvss 7989 tz7.48-1 8274 enssdom 8765 enfii 8972 fineqvlem 9037 infcntss 9088 infeq5 9395 omex 9401 rankuni 9621 scott0 9644 acni3 9803 acnnum 9808 dfac3 9877 dfac9 9892 kmlem1 9906 cflm 10006 cfcof 10030 axdc4lem 10211 axcclem 10213 ac6c4 10237 ac6s 10240 ac6s2 10242 axdclem2 10276 brdom3 10284 brdom5 10285 brdom4 10286 nqpr 10770 ltexprlem4 10795 reclem2pr 10804 hash1to3 14205 trclublem 14706 fnpr2ob 17269 drsdirfi 18023 toprntopon 22074 2ndcsb 22600 fbssint 22989 isfil2 23007 alexsubALTlem3 23200 lpbl 23659 metustfbas 23713 ex-natded9.26-2 28784 19.9d2rf 30820 rexunirn 30840 f1ocnt 31123 fsumiunle 31143 fmcncfil 31881 esumiun 32062 0elsiga 32082 ddemeas 32204 bnj168 32709 bnj593 32725 bnj607 32896 bnj600 32899 bnj916 32913 fineqvpow 33065 lfuhgr3 33081 cusgredgex 33083 loop1cycl 33099 umgr2cycl 33103 fundmpss 33740 lrrecfr 34100 exisym1 34613 bj-sylge 34805 bj-19.12 34943 bj-equs45fv 34993 bj-snsetex 35153 bj-snglss 35160 bj-snglex 35163 bj-bm1.3ii 35235 bj-restn0 35261 bj-ccinftydisj 35384 mptsnunlem 35509 pibt2 35588 wl-cbvmotv 35672 wl-moae 35675 wl-nax6im 35677 sn-iotanul 40194 iscard4 41140 ismnushort 41919 spsbce-2 41999 iotaexeu 42036 iotasbc 42037 relopabVD 42521 ax6e2ndeqVD 42529 2uasbanhVD 42531 ax6e2ndeqALT 42551 fnchoice 42572 rfcnnnub 42579 stoweidlem35 43576 stoweidlem57 43598 mo0sn 46161 |
Copyright terms: Public domain | W3C validator |