![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimivv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
Ref | Expression |
---|---|
rexlimivv.1 | ⊢ ((x ∈ A ∧ y ∈ B) → (φ → ψ)) |
Ref | Expression |
---|---|
rexlimivv | ⊢ (∃x ∈ A ∃y ∈ B φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivv.1 | . . 3 ⊢ ((x ∈ A ∧ y ∈ B) → (φ → ψ)) | |
2 | 1 | rexlimdva 2427 | . 2 ⊢ (x ∈ A → (∃y ∈ B φ → ψ)) |
3 | 2 | rexlimiv 2421 | 1 ⊢ (∃x ∈ A ∃y ∈ B φ → ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1390 ∃wrex 2301 |
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-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-i5r 1425 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 df-rex 2306 |
This theorem is referenced by: opelxp 4317 f1o2ndf1 5791 xpdom2 6241 distrlem5prl 6562 distrlem5pru 6563 mulid1 6822 cnegex 6986 recexap 7416 creur 7692 creui 7693 cju 7694 elz2 8088 qre 8336 qaddcl 8346 qnegcl 8347 qmulcl 8348 qreccl 8351 replim 9087 |
Copyright terms: Public domain | W3C validator |