![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eeanv | GIF version |
Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) |
Ref | Expression |
---|---|
eeanv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1467 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1467 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | eean 1855 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1427 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 |
This theorem depends on definitions: df-bi 116 df-nf 1396 |
This theorem is referenced by: eeeanv 1857 ee4anv 1858 2eu4 2042 cgsex2g 2658 cgsex4g 2659 vtocl2 2677 spc2egv 2711 spc2gv 2712 dtruarb 4034 copsex2t 4083 copsex2g 4084 opelopabsb 4098 xpmlem 4867 fununi 5097 imain 5111 brabvv 5711 spc2ed 6014 tfrlem7 6098 ener 6552 domtr 6558 unen 6589 mapen 6618 sbthlemi10 6731 ltexprlemdisj 7228 recexprlemdisj 7252 hashfacen 10304 isummo 10836 |
Copyright terms: Public domain | W3C validator |