![]() |
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 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimivv | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivv.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) | |
2 | 1 | rexlimdva 2490 | . 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | rexlimiv 2484 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1439 ∃wrex 2361 |
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-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-i5r 1474 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-ral 2365 df-rex 2366 |
This theorem is referenced by: opelxp 4481 f1o2ndf1 6007 xpdom2 6601 distrlem5prl 7206 distrlem5pru 7207 mulid1 7546 cnegex 7721 recexap 8183 creur 8480 creui 8481 cju 8482 elz2 8879 qre 9171 qaddcl 9181 qnegcl 9182 qmulcl 9183 qreccl 9188 replim 10354 odd2np1 11212 opoe 11234 omoe 11235 opeo 11236 omeo 11237 qredeu 11418 |
Copyright terms: Public domain | W3C validator |