![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exancom | 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 266 | . 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
2 | 1 | exbii 1605 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.29r 1621 19.42h 1687 19.42 1688 risset 2505 morex 2923 dfuni2 3813 eluni2 3815 unipr 3825 dfiun2g 3920 uniuni 4453 cnvco 4814 imadif 5298 funimaexglem 5301 pceu 12297 bdcuni 14713 bj-axun2 14752 |
Copyright terms: Public domain | W3C validator |