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 2394 axc11n 2443 bm1.3ii 5198 axprlem1 5315 axprlem2 5316 axpr 5320 inf3 9087 epfrs 9162 kmlem2 9566 axcc2lem 9847 dcomex 9858 axdclem2 9931 grothpw 10237 grothpwex 10238 grothomex 10240 grothac 10241 cnso 15590 aannenlem3 24848 bj-ax12 33888 bj-ax6e 33899 wl-spae 34644 |
Copyright terms: Public domain | W3C validator |