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 1840 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | |
2 | eximi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1804 | 1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 |
This theorem depends on definitions: df-bi 210 df-ex 1787 |
This theorem is referenced by: 2eximi 1842 eximii 1843 exa1 1844 exsimpl 1874 exsimpr 1875 19.29r2 1881 19.29x 1882 19.35 1883 19.40-2 1893 emptyex 1913 exlimiv 1936 speimfwALT 1971 19.12 2328 ax13lem2 2375 exdistrf 2446 equs45f 2458 dfmoeu 2536 moimi 2545 eu6 2575 2eu2ex 2646 reximi2 3157 cgsexg 3439 gencbvex 3452 eqvincg 3542 n0rex 4241 axrep2 5154 bm1.3ii 5167 ax6vsep 5168 copsexgw 5344 copsexg 5345 relopabi 5660 dminss 5979 imainss 5980 iotaex 6313 fv3 6686 ssimaex 6747 dffv2 6757 exfo 6875 oprabidw 7195 oprabid 7196 zfrep6 7674 frxp 7839 suppimacnvss 7861 tz7.48-1 8101 enssdom 8573 enfii 8777 fineqvlem 8804 infcntss 8859 infeq5 9166 omex 9172 rankuni 9358 scott0 9381 acni3 9540 acnnum 9545 dfac3 9614 dfac9 9629 kmlem1 9643 cflm 9743 cfcof 9767 axdc4lem 9948 axcclem 9950 ac6c4 9974 ac6s 9977 ac6s2 9979 axdclem2 10013 brdom3 10021 brdom5 10022 brdom4 10023 nqpr 10507 ltexprlem4 10532 reclem2pr 10541 hash1to3 13936 trclublem 14437 fnpr2ob 16927 drsdirfi 17657 toprntopon 21669 2ndcsb 22193 fbssint 22582 isfil2 22600 alexsubALTlem3 22793 lpbl 23249 metustfbas 23303 ex-natded9.26-2 28349 19.9d2rf 30386 rexunirn 30406 f1ocnt 30690 fsumiunle 30710 fmcncfil 31445 esumiun 31624 0elsiga 31644 ddemeas 31766 bnj168 32271 bnj593 32287 bnj607 32459 bnj600 32462 bnj916 32476 fineqvpow 32628 lfuhgr3 32644 cusgredgex 32646 loop1cycl 32662 umgr2cycl 32666 fundmpss 33304 lrrecfr 33729 exisym1 34243 bj-sylge 34432 bj-19.12 34570 bj-equs45fv 34613 bj-snsetex 34765 bj-snglss 34772 bj-snglex 34775 bj-bm1.3ii 34847 bj-restn0 34871 bj-ccinftydisj 34994 mptsnunlem 35121 pibt2 35200 wl-cbvmotv 35284 wl-moae 35287 wl-nax6im 35289 iscard4 40678 spsbce-2 41521 iotaexeu 41558 iotasbc 41559 relopabVD 42043 ax6e2ndeqVD 42051 2uasbanhVD 42053 ax6e2ndeqALT 42073 fnchoice 42094 rfcnnnub 42101 stoweidlem35 43102 stoweidlem57 43124 mo0sn 45677 |
Copyright terms: Public domain | W3C validator |