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 1506 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) | |
2 | 1 | 19.41h 1663 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.41vv 1875 19.41vvv 1876 19.41vvvv 1877 exdistrv 1882 eeeanv 1903 gencbvex 2727 euxfrdc 2865 euind 2866 dfdif3 3181 r19.9rmv 3449 opabm 4197 eliunxp 4673 relop 4684 dmuni 4744 dmres 4835 dminss 4948 imainss 4949 ssrnres 4976 cnvresima 5023 resco 5038 rnco 5040 coass 5052 xpcom 5080 f11o 5393 fvelrnb 5462 rnoprab 5847 domen 6638 xpassen 6717 genpassl 7325 genpassu 7326 |
Copyright terms: Public domain | W3C validator |