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 2237 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 1848 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓)) |
3 | 19.41v 1950 | . 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | |
4 | 2, 3 | bitri 277 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 |
This theorem is referenced by: 19.41vvv 1952 rabxp 5600 copsex2gb 5679 mpomptx 7265 xpassen 8611 dfac5lem1 9549 fusgr2wsp2nb 28113 bnj996 32228 dfdm5 33016 dfrn5 33017 elima4 33019 brtxp2 33342 brpprod3a 33347 brimg 33398 brsuccf 33402 brxrn2 35642 diblsmopel 38322 en2pr 39926 mpomptx2 44403 |
Copyright terms: Public domain | W3C validator |