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 1841. (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 1841 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 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: exan 1868 spimehOLD 1979 exgenOLD 1983 ax6evr 2026 spimedv 2198 spimfv 2240 ax6e 2382 spim 2386 spimed 2387 spimvALT 2390 spei 2393 equvini 2454 equvel 2455 euequ 2598 dariiALT 2668 barbariALT 2672 festinoALT 2677 barocoALT 2679 daraptiALT 2687 vtoclf 3462 axrep2 5154 axnul 5170 nalset 5178 notzfaus 5225 notzfausOLD 5226 el 5233 dtru 5234 dvdemo1 5237 dvdemo2 5238 eusv2nf 5259 axprALT 5286 axpr 5292 inf1 9151 bnd 9387 axpowndlem2 10091 grothomex 10322 tgjustc1 26413 tgjustc2 26414 bnj101 32264 axextdfeq 33337 ax8dfeq 33338 axextndbi 33344 snelsingles 33854 bj-ax6elem2 34475 bj-dtru 34619 ax6er 34636 bj-vtoclf 34721 wl-exeq 35305 sn-el 39762 spd 45821 elpglem2 45854 eximp-surprise2 45926 |
Copyright terms: Public domain | W3C validator |