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 257 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝜓 → 𝜒))) |
3 | 2 | rexlimdv 2548 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
4 | 3 | rexlimdva 2549 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1480 ∃wrex 2417 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2421 df-rex 2422 |
This theorem is referenced by: rexlimdvva 2557 f1oiso2 5728 xpdom2 6725 genpcdl 7327 genpcuu 7328 distrlem1prl 7390 distrlem1pru 7391 distrlem5prl 7394 distrlem5pru 7395 recexprlemss1l 7443 recexprlemss1u 7444 qaddcl 9427 qmulcl 9429 summodc 11152 dvdsgcd 11700 gcddiv 11707 txcnp 12440 blssps 12596 blss 12597 tgqioo 12716 |
Copyright terms: Public domain | W3C validator |