| 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 482 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 2 | 1 | eximi 1835 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: 19.40 1886 moexexlem 2626 elissetv 2822 clelab 2887 elexOLD 3502 sbc5ALT 3817 r19.2zb 4496 dmcoss 5985 suppimacnvss 8198 unblem2 9329 kmlem8 10198 isssc 17864 krull 33507 bnj1143 34804 bnj1371 35043 bnj1374 35045 atex 39408 rtrclex 43630 clcnvlem 43636 pm10.55 44388 |
| Copyright terms: Public domain | W3C validator |