![]() |
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 2278 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 2048 | . . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓)) | |
2 | 1 | exbii 1947 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓)) |
3 | 19.41v 2048 | . 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | |
4 | 2, 3 | bitri 267 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∃wex 1878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 |
This theorem is referenced by: 19.41vvv 2050 rabxp 5391 copsex2gb 5468 mpt2mptx 7016 xpassen 8329 dfac5lem1 9266 fusgr2wsp2nb 27711 bnj996 31567 dfdm5 32209 dfrn5 32210 elima4 32212 brtxp2 32522 brpprod3a 32527 brimg 32578 brsuccf 32582 brxrn2 34680 diblsmopel 37241 mpt2mptx2 42974 |
Copyright terms: Public domain | W3C validator |