![]() |
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 461 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
2 | 1 | exbii 1850 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ 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.42v 1957 19.42 2229 eupickb 2635 datisi 2679 disamis 2680 dimatis 2687 fresison 2688 bamalip 2691 risset 3220 morex 3676 pwpw0 4772 pwsnOLD 4857 dfuni2 4866 eluni2 4868 uniprOLD 4883 dfiun2gOLD 4990 cnvco 5840 imadif 6583 uniuni 7693 pceu 16715 gsumval3eu 19677 isch3 30081 tgoldbachgt 33167 bnj1109 33289 bnj1304 33322 bnj849 33428 funpartlem 34516 bj-19.41t 35228 bj-elsngl 35428 bj-ccinftydisj 35673 mopickr 36813 moantr 36814 brcosscnvcoss 36885 rr-groth 42559 rr-grothshortbi 42563 eluni2f 43293 ssfiunibd 43517 setrec1lem3 47104 |
Copyright terms: Public domain | W3C validator |