![]() |
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 1832 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 |
This theorem is referenced by: 19.40 1884 moexexlem 2624 elissetv 2820 clelab 2885 elexOLD 3500 sbc5ALT 3820 r19.2zb 4502 dmcoss 5988 suppimacnvss 8197 unblem2 9327 kmlem8 10196 isssc 17868 krull 33487 bnj1143 34783 bnj1371 35022 bnj1374 35024 atex 39389 rtrclex 43607 clcnvlem 43613 pm10.55 44365 |
Copyright terms: Public domain | W3C validator |