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 1837. (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 1837 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 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: exan 1865 ax6evr 2018 spimedv 2190 spimfv 2232 ax6e 2383 spim 2387 spimed 2388 spimvALT 2391 spei 2394 equvini 2455 equvel 2456 euequ 2597 dariiALT 2667 barbariALT 2671 festinoALT 2676 barocoALT 2678 daraptiALT 2686 vtoclf 3497 axrep2 5212 axnul 5229 nalset 5237 notzfaus 5285 elALT2 5292 dtruALT2 5293 dvdemo1 5296 dvdemo2 5297 eusv2nf 5318 axprALT 5345 axpr 5351 dtru 5359 inf1 9380 bnd 9650 axpowndlem2 10354 grothomex 10585 tgjustc1 26836 tgjustc2 26837 bnj101 32702 axextdfeq 33773 ax8dfeq 33774 axextndbi 33780 snelsingles 34224 bj-ax6elem2 34848 bj-dtru 34999 ax6er 35016 bj-vtoclf 35100 wl-exeq 35693 sn-el 40187 spd 46384 elpglem2 46417 eximp-surprise2 46489 |
Copyright terms: Public domain | W3C validator |