| 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 2237 eupickb 2628 datisi 2673 disamis 2674 dimatis 2681 fresison 2682 bamalip 2685 risset 3204 morex 3679 pwpw0 4764 dfuni2 4860 eluni2 4862 cnvco 5828 imadif 6566 uniuni 7698 pceu 16758 gsumval3eu 19783 isch3 31185 tgoldbachgt 34637 bnj1109 34759 bnj1304 34792 bnj849 34898 onvf1odlem1 35086 funpartlem 35926 bj-19.41t 36758 bj-elsngl 36952 bj-ccinftydisj 37197 mopickr 38341 moantr 38342 brcosscnvcoss 38421 rr-groth 44282 rr-grothshortbi 44286 eluni2f 45091 ssfiunibd 45301 setrec1lem3 49684 |
| Copyright terms: Public domain | W3C validator |