![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimdvaa | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.) |
Ref | Expression |
---|---|
rexlimdvaa.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) |
Ref | Expression |
---|---|
rexlimdvaa | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvaa.1 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) | |
2 | 1 | expr 375 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
3 | 2 | rexlimdva 2594 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 ∃wrex 2456 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 df-rex 2461 |
This theorem is referenced by: rexlimddv 2599 nnsucuniel 6490 omp1eomlem 7087 ctmlemr 7101 mulgt0sr 7765 axpre-suploclemres 7888 cnegex 8122 receuap 8612 recapb 8614 rexanuz 10978 climcaucn 11340 fsumiun 11466 dvdsval2 11778 prmind2 12100 pcprmpw2 12312 pockthg 12335 dvdsrvald 13084 dvdsrd 13085 dvdsrex 13089 unitgrp 13107 tgcl 13224 neiint 13305 restopnb 13341 iscnp4 13378 blssexps 13589 blssex 13590 lgsne0 14099 |
Copyright terms: Public domain | W3C validator |