![]() |
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 2235 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 1950 | . . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓)) | |
2 | 1 | exbii 1849 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓)) |
3 | 19.41v 1950 | . 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | |
4 | 2, 3 | bitri 278 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 |
This theorem is referenced by: 19.41vvv 1952 rabxp 5564 copsex2gb 5643 mpomptx 7244 xpassen 8594 dfac5lem1 9534 fusgr2wsp2nb 28119 bnj996 32338 dfdm5 33129 dfrn5 33130 elima4 33132 brtxp2 33455 brpprod3a 33460 brimg 33511 brsuccf 33515 brxrn2 35787 diblsmopel 38467 en2pr 40246 mpomptx2 44736 |
Copyright terms: Public domain | W3C validator |