![]() |
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 1466 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1466 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | eean 1854 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∃wex 1426 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 df-nf 1395 |
This theorem is referenced by: eeeanv 1856 ee4anv 1857 2eu4 2041 cgsex2g 2655 cgsex4g 2656 vtocl2 2674 spc2egv 2708 spc2gv 2709 dtruarb 4026 copsex2t 4072 copsex2g 4073 opelopabsb 4087 xpmlem 4852 fununi 5082 imain 5096 brabvv 5695 spc2ed 5998 tfrlem7 6082 ener 6494 domtr 6500 unen 6531 mapen 6560 sbthlemi10 6673 ltexprlemdisj 7163 recexprlemdisj 7187 hashfacen 10237 isummo 10769 |
Copyright terms: Public domain | W3C validator |