Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimdv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Ref | Expression |
---|---|
rexlimdv.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
rexlimdv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | rexlimdv.1 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
4 | 1, 2, 3 | rexlimd 2430 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ∃wrex 2307 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 df-rex 2312 |
This theorem is referenced by: rexlimdva 2433 rexlimdv3a 2435 rexlimdvw 2436 rexlimdvv 2439 trintssm 3870 ssorduni 4213 funcnvuni 4968 dffo3 5314 smoiun 5916 tfrlem9 5935 ordiso2 6357 axprecex 6954 recexap 7634 zdiv 8328 btwnz 8357 lbzbi 8551 |
Copyright terms: Public domain | W3C validator |