![]() |
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 2501 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
4 | 3 | rexlimdva 2502 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1445 ∃wrex 2371 |
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 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 ax-i5r 1480 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-ral 2375 df-rex 2376 |
This theorem is referenced by: rexlimdvva 2510 f1oiso2 5644 xpdom2 6627 genpcdl 7175 genpcuu 7176 distrlem1prl 7238 distrlem1pru 7239 distrlem5prl 7242 distrlem5pru 7243 recexprlemss1l 7291 recexprlemss1u 7292 qaddcl 9219 qmulcl 9221 summodc 10941 dvdsgcd 11443 gcddiv 11450 blssps 12228 blss 12229 tgqioo 12336 |
Copyright terms: Public domain | W3C validator |