![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimdvv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.) |
Ref | Expression |
---|---|
rexlimdvv.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
rexlimdvv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvv.1 | . . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) | |
2 | 1 | expdimp 256 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒))) |
3 | 2 | rexlimdv 2490 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
4 | 3 | rexlimdva 2491 | 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: rexlimdvva 2499 f1oiso2 5622 xpdom2 6603 genpcdl 7141 genpcuu 7142 distrlem1prl 7204 distrlem1pru 7205 distrlem5prl 7208 distrlem5pru 7209 recexprlemss1l 7257 recexprlemss1u 7258 qaddcl 9183 qmulcl 9185 isummo 10836 dvdsgcd 11342 gcddiv 11349 |
Copyright terms: Public domain | W3C validator |