![]() |
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 1838. (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 1838 | . 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 1866 ax6evr 2019 spimedv 2191 spimfv 2233 ax6e 2383 spim 2387 spimed 2388 spimvALT 2391 spei 2394 equvini 2455 equvel 2456 euequ 2592 dariiALT 2662 barbariALT 2666 festinoALT 2671 barocoALT 2673 daraptiALT 2681 vtoclfOLD 3547 axrep2 5284 axnul 5301 nalset 5309 notzfaus 5357 elALT2 5363 dtruALT2 5364 dvdemo1 5367 dvdemo2 5368 eusv2nf 5389 axprALT 5416 axpr 5422 exel 5429 dtruOLD 5437 inf1 9604 bnd 9874 axpowndlem2 10580 grothomex 10811 tgjustc1 27693 tgjustc2 27694 bnj101 33665 axextdfeq 34700 ax8dfeq 34701 axextndbi 34707 snelsingles 34825 bj-ax6elem2 35449 ax6er 35616 bj-vtoclf 35700 wl-exeq 36308 sn-exelALT 40951 spd 47563 elpglem2 47597 eximp-surprise2 47672 |
Copyright terms: Public domain | W3C validator |