![]() |
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 1474 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | 1 | 19.41h 1631 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1436 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.41vv 1842 19.41vvv 1843 19.41vvvv 1844 exdistrv 1847 eeeanv 1868 gencbvex 2687 euxfrdc 2823 euind 2824 dfdif3 3133 r19.9rmv 3401 opabm 4140 eliunxp 4616 relop 4627 dmuni 4687 dmres 4776 dminss 4889 imainss 4890 ssrnres 4917 cnvresima 4964 resco 4979 rnco 4981 coass 4993 xpcom 5021 f11o 5334 fvelrnb 5401 rnoprab 5786 domen 6575 xpassen 6653 genpassl 7233 genpassu 7234 |
Copyright terms: Public domain | W3C validator |