| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exancom | Structured version Visualization version GIF version | ||
| Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
| Ref | Expression |
|---|---|
| exancom | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ancom 460 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
| 2 | 1 | exbii 1848 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ 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.42v 1953 19.42 2236 eupickb 2635 datisi 2680 disamis 2681 dimatis 2688 fresison 2689 bamalip 2692 risset 3233 morex 3725 pwpw0 4813 dfuni2 4909 eluni2 4911 dfiun2gOLD 5031 cnvco 5896 imadif 6650 uniuni 7782 pceu 16884 gsumval3eu 19922 isch3 31260 tgoldbachgt 34678 bnj1109 34800 bnj1304 34833 bnj849 34939 funpartlem 35943 bj-19.41t 36775 bj-elsngl 36969 bj-ccinftydisj 37214 mopickr 38364 moantr 38365 brcosscnvcoss 38435 rr-groth 44318 rr-grothshortbi 44322 eluni2f 45108 ssfiunibd 45321 setrec1lem3 49208 |
| Copyright terms: Public domain | W3C validator |