![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exsimpl | Structured version Visualization version GIF version |
Description: Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
exsimpl | ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 475 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | eximi 1797 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∃wex 1742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 |
This theorem is referenced by: 19.40 1849 euexALTOLD 2642 moexexvw 2661 2moswapv 2662 moexex 2669 elisset 3426 elex 3433 sbc5 3708 r19.2zb 4325 dmcoss 5685 suppimacnvss 7645 unblem2 8568 kmlem8 9379 isssc 16951 bnj1143 31710 bnj1371 31946 bnj1374 31948 bj-elissetv 33684 atex 35987 rtrclex 39340 clcnvlem 39346 pm10.55 40117 |
Copyright terms: Public domain | W3C validator |