| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 19.42vv | Structured version Visualization version GIF version | ||
| Description: Version of 19.42 2236 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
| Ref | Expression |
|---|---|
| 19.42vv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exdistr 1954 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
| 2 | 19.42v 1953 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 |
| This theorem is referenced by: exdistr2 1958 3exdistr 1960 cgsex4g 3528 ceqsex3v 3537 ceqsex4v 3538 ceqsex8v 3540 elvvv 5761 xpdifid 6188 dfoprab2 7491 resoprab 7551 elrnmpores 7571 ov3 7596 ov6g 7597 oprabex3 8002 xpassen 9106 entrfil 9225 domtrfil 9232 sbthfilem 9238 axaddf 11185 axmulf 11186 catcone0 17730 qqhval2 33983 bnj996 34970 fineqvac 35111 inxpxrn 38396 dvhopellsm 41119 |
| Copyright terms: Public domain | W3C validator |