![]() |
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 1836 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 |
This theorem is referenced by: 19.40 1888 moexexlem 2621 elissetv 2813 clelab 2878 elex 3492 sbc5ALT 3806 r19.2zb 4495 dmcoss 5970 suppimacnvss 8163 unblem2 9302 kmlem8 10158 isssc 17774 krull 33033 bnj1143 34264 bnj1371 34503 bnj1374 34505 atex 38740 rtrclex 42830 clcnvlem 42836 pm10.55 43590 |
Copyright terms: Public domain | W3C validator |