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 1839 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 |
This theorem is referenced by: 19.42v 1945 19.42 2228 eupickb 2713 datisi 2760 disamis 2761 dimatis 2768 fresison 2769 bamalip 2772 risset 3264 morex 3707 pwpw0 4738 pwsnALT 4823 dfuni2 4832 eluni2 4834 unipr 4843 dfiun2g 4946 dfiun2gOLD 4947 cnvco 5749 imadif 6431 uniuni 7473 pceu 16171 gsumval3eu 18953 isch3 28945 tgoldbachgt 31833 bnj1109 31957 bnj1304 31990 bnj849 32096 funpartlem 33300 bj-19.41t 34000 bj-elsngl 34177 bj-ccinftydisj 34387 moantr 35497 brcosscnvcoss 35559 rr-groth 40512 eluni2f 41246 ssfiunibd 41452 setrec1lem3 44720 |
Copyright terms: Public domain | W3C validator |