![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exlimiiv | Structured version Visualization version GIF version |
Description: Inference associated with exlimiv 1995. (Contributed by BJ, 19-Dec-2020.) |
Ref | Expression |
---|---|
exlimiv.1 | ⊢ (𝜑 → 𝜓) |
exlimiiv.2 | ⊢ ∃𝑥𝜑 |
Ref | Expression |
---|---|
exlimiiv | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimiiv.2 | . 2 ⊢ ∃𝑥𝜑 | |
2 | exlimiv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | exlimiv 1995 | . 2 ⊢ (∃𝑥𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 |
This theorem depends on definitions: df-bi 197 df-ex 1842 |
This theorem is referenced by: equid 2082 ax7 2086 ax12v2 2186 19.8a 2187 ax6e 2383 axc11n 2439 axc11nOLD 2440 axext3 2730 bm1.3ii 4924 inf3 8693 epfrs 8768 kmlem2 9136 axcc2lem 9421 dcomex 9432 axdclem2 9505 grothpw 9811 grothpwex 9812 grothomex 9814 grothac 9815 cnso 15146 aannenlem3 24255 bj-ax6e 32930 wl-spae 33588 |
Copyright terms: Public domain | W3C validator |