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 1421 | . 2 ⊢ Ⅎ𝑦𝜑 | |
2 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | 1, 2 | eean 1806 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: eeeanv 1808 ee4anv 1809 2eu4 1993 cgsex2g 2590 cgsex4g 2591 vtocl2 2609 spc2egv 2642 spc2gv 2643 dtruarb 3942 copsex2t 3982 copsex2g 3983 opelopabsb 3997 xpmlem 4744 fununi 4967 imain 4981 brabvv 5551 tfrlem7 5933 ener 6259 domtr 6265 unen 6293 ltexprlemdisj 6704 recexprlemdisj 6728 |
Copyright terms: Public domain | W3C validator |