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 1521 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1521 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | rexlimdv.1 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
4 | 1, 2, 3 | rexlimd 2584 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∃wrex 2449 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 df-rex 2454 |
This theorem is referenced by: rexlimdva 2587 rexlimdv3a 2589 rexlimdva2 2590 rexlimdvw 2591 rexlimdvv 2594 ssorduni 4471 funcnvuni 5267 dffo3 5643 smoiun 6280 tfrlem9 6298 ordiso2 7012 axprecex 7842 recexap 8571 zdiv 9300 btwnz 9331 lbzbi 9575 neibl 13285 metcnp3 13305 |
Copyright terms: Public domain | W3C validator |