![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.41vv | Structured version Visualization version GIF version |
Description: Version of 19.41 2224 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
Ref | Expression |
---|---|
19.41vv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.41v 1946 | . . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓)) | |
2 | 1 | exbii 1843 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓)) |
3 | 19.41v 1946 | . 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | |
4 | 2, 3 | bitri 274 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 |
This theorem is referenced by: 19.41vvv 1948 cgsex4g 3513 rabxp 5722 copsex2gb 5804 mpomptx 7529 xpassen 9095 dfac5lem1 10158 fusgr2wsp2nb 30263 bnj996 34813 dfdm5 35608 dfrn5 35609 elima4 35611 brtxp2 35717 brpprod3a 35722 brimg 35773 brsuccf 35777 brxrn2 38085 diblsmopel 40882 en2pr 43250 mpomptx2 47748 |
Copyright terms: Public domain | W3C validator |