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 2105 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
19.42vv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr 1919 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
2 | 19.42v 1918 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | |
3 | 1, 2 | bitri 264 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ∃wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: 19.42vvv 1921 exdistr2 1922 3exdistr 1923 ceqsex3v 3246 ceqsex4v 3247 ceqsex8v 3249 elvvv 5178 xpdifid 5562 dfoprab2 6701 resoprab 6756 elrnmpt2res 6774 ov3 6797 ov6g 6798 oprabex3 7157 xpassen 8054 axaddf 9966 axmulf 9967 qqhval2 30026 bnj996 31025 dvhopellsm 36406 |
Copyright terms: Public domain | W3C validator |