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 1831. (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 1831 | . 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ∃𝑥𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 209 df-ex 1777 |
This theorem is referenced by: exan 1858 exanOLD 1859 spimehOLD 1971 exgenOLD 1975 ax6evr 2018 spimedv 2192 spimfv 2236 ax6e 2397 spim 2401 spimed 2402 spimvALT 2405 spei 2408 equvini 2473 equviniOLD 2474 equvel 2475 equsb1vOLDOLD 2513 euequ 2679 dariiALT 2749 barbariALT 2753 festinoALT 2758 barocoALT 2760 daraptiALT 2768 vtoclf 3559 vtocl 3560 axrep2 5186 axnul 5202 nalset 5210 notzfaus 5255 notzfausOLD 5256 el 5263 dtru 5264 dvdemo1 5267 dvdemo2 5268 eusv2nf 5288 axprALT 5315 axpr 5321 inf1 9079 bnd 9315 axpowndlem2 10014 grothomex 10245 tgjustc1 26255 tgjustc2 26256 bnj101 31988 axextdfeq 33037 ax8dfeq 33038 axextndbi 33044 snelsingles 33378 bj-ax6elem2 33995 bj-dtru 34134 ax6er 34151 bj-vtoclf 34226 wl-exeq 34768 sn-el 39103 spd 44774 elpglem2 44807 eximp-surprise2 44879 |
Copyright terms: Public domain | W3C validator |