![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eximii | Structured version Visualization version GIF version |
Description: Inference associated with eximi 1802. (Contributed by BJ, 3-Feb-2018.) |
Ref | Expression |
---|---|
eximii.1 | ⊢ ∃𝑥𝜑 |
eximii.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
eximii | ⊢ ∃𝑥𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximii.1 | . 2 ⊢ ∃𝑥𝜑 | |
2 | eximii.2 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | eximi 1802 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 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: exiftru 1948 spimeh 1971 ax6evr 1988 spimv1 2153 ax6e 2286 spim 2290 spimed 2291 spimv 2293 spei 2297 equvini 2374 equvel 2375 euequ1 2504 euex 2522 darii 2594 barbari 2596 festino 2600 baroco 2601 cesaro 2602 camestros 2603 datisi 2604 disamis 2605 felapton 2608 darapti 2609 dimatis 2611 fresison 2612 calemos 2613 fesapo 2614 bamalip 2615 vtoclf 3289 vtocl 3290 axrep2 4806 axnul 4821 nalset 4828 notzfaus 4870 el 4877 dtru 4887 eusv2nf 4894 dvdemo1 4932 dvdemo2 4933 axpr 4935 snnexOLD 7009 inf1 8557 bnd 8793 axpowndlem2 9458 grothomex 9689 bnj101 30917 axextdfeq 31827 ax8dfeq 31828 axextndbi 31834 snelsingles 32154 bj-ax6elem2 32777 bj-spimedv 32844 bj-spimvv 32846 bj-speiv 32849 bj-axrep2 32914 bj-nalset 32919 bj-el 32921 bj-dtru 32922 bj-dvdemo1 32927 bj-dvdemo2 32928 ax6er 32945 bj-vtoclf 33033 wl-exeq 33451 spd 42750 elpglem2 42783 eximp-surprise2 42859 |
Copyright terms: Public domain | W3C validator |