![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.41v | GIF version |
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.41v | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1537 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | 1 | 19.41h 1696 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∃wex 1503 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.41vv 1915 19.41vvv 1916 19.41vvvv 1917 exdistrv 1922 eeeanv 1949 gencbvex 2807 euxfrdc 2947 euind 2948 dfdif3 3270 r19.9rmv 3539 opabm 4312 eliunxp 4802 relop 4813 dmuni 4873 dmres 4964 dminss 5081 imainss 5082 ssrnres 5109 cnvresima 5156 resco 5171 rnco 5173 coass 5185 xpcom 5213 f11o 5534 fvelrnb 5605 rnoprab 6002 domen 6807 xpassen 6886 genpassl 7586 genpassu 7587 |
Copyright terms: Public domain | W3C validator |