![]() |
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 1973. (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 1973 | . 2 ⊢ (∃𝑥𝜑 → 𝜓) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: equid 2059 ax7 2063 ax12v2 2165 19.8a 2166 ax6e 2347 axc11n 2392 sbcom2 2523 axext3 2756 bm1.3ii 5022 inf3 8831 epfrs 8906 kmlem2 9310 axcc2lem 9595 dcomex 9606 axdclem2 9679 grothpw 9985 grothpwex 9986 grothomex 9988 grothac 9989 cnso 15384 aannenlem3 24526 bj-ax6e 33247 wl-spae 33905 |
Copyright terms: Public domain | W3C validator |