![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.42vv | GIF version |
Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
19.42vv | ⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr 1784 | . 2 ⊢ (∃x∃y(φ ∧ ψ) ↔ ∃x(φ ∧ ∃yψ)) | |
2 | 19.42v 1783 | . 2 ⊢ (∃x(φ ∧ ∃yψ) ↔ (φ ∧ ∃x∃yψ)) | |
3 | 1, 2 | bitri 173 | 1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 ∃wex 1378 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 19.42vvv 1786 19.42vvvv 1787 exdistr2 1788 3exdistr 1789 ceqsex3v 2590 ceqsex4v 2591 elvvv 4346 dfoprab2 5494 resoprab 5539 ovi3 5579 ov6g 5580 oprabex3 5698 xpassen 6240 enq0enq 6414 enq0sym 6415 nqnq0pi 6421 |
Copyright terms: Public domain | W3C validator |