![]() |
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 | ⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1418 | . 2 ⊢ Ⅎyφ | |
2 | nfv 1418 | . 2 ⊢ Ⅎxψ | |
3 | 1, 2 | eean 1803 | 1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 ∃wex 1378 |
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 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: eeeanv 1805 ee4anv 1806 2eu4 1990 cgsex2g 2584 cgsex4g 2585 vtocl2 2603 spc2egv 2636 spc2gv 2637 dtruarb 3933 copsex2t 3973 copsex2g 3974 opelopabsb 3988 xpmlem 4687 fununi 4910 imain 4924 brabvv 5493 tfrlem7 5874 ener 6195 domtr 6201 unen 6229 ltexprlemdisj 6580 recexprlemdisj 6602 |
Copyright terms: Public domain | W3C validator |