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 1922. (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 1922 | . 2 ⊢ (∃𝑥𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: equid 2010 ax7 2014 sbcom2 2158 ax12v2 2169 19.8a 2170 ax6e 2392 axc11n 2440 bm1.3ii 5197 axprlem1 5314 axprlem2 5315 axpr 5319 inf3 9086 epfrs 9161 kmlem2 9565 axcc2lem 9846 dcomex 9857 axdclem2 9930 grothpw 10236 grothpwex 10237 grothomex 10239 grothac 10240 cnso 15588 aannenlem3 24846 bj-ax12 33887 bj-ax6e 33898 wl-spae 34643 |
Copyright terms: Public domain | W3C validator |