![]() |
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 483 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | eximi 1837 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 |
This theorem is referenced by: 19.40 1889 moexexlem 2622 elissetv 2814 clelab 2879 elex 3492 sbc5ALT 3806 r19.2zb 4495 dmcoss 5970 suppimacnvss 8157 unblem2 9295 kmlem8 10151 isssc 17766 krull 32589 bnj1143 33796 bnj1371 34035 bnj1374 34037 atex 38272 rtrclex 42358 clcnvlem 42364 pm10.55 43118 |
Copyright terms: Public domain | W3C validator |