![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exlimiiv | Structured version Visualization version GIF version |
Description: Inference (Rule C) associated with exlimiv 1933. (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 1933 | . 2 ⊢ (∃𝑥𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: equid 2015 ax7 2019 sbcom2 2161 ax12v2 2173 19.8a 2174 ax6e 2381 axc11n 2424 vtocl 3546 bm1.3ii 5295 axprlem1 5414 axprlem2 5415 axpr 5419 inf3 9612 epfrs 9708 kmlem2 10128 axcc2lem 10413 dcomex 10424 axdclem2 10497 grothpw 10803 grothpwex 10804 grothomex 10806 grothac 10807 cnso 16172 aannenlem3 25772 bj-ax12 35336 bj-ax6e 35347 wl-spae 36192 |
Copyright terms: Public domain | W3C validator |