![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > rexlimdva | Structured version GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
Ref | Expression |
---|---|
rexlimdva.1 | ⊢ ((φ ∧ x ∈ A) → (ψ → χ)) |
Ref | Expression |
---|---|
rexlimdva | ⊢ (φ → (∃x ∈ A ψ → χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdva.1 | . . 3 ⊢ ((φ ∧ x ∈ A) → (ψ → χ)) | |
2 | 1 | ex 108 | . 2 ⊢ (φ → (x ∈ A → (ψ → χ))) |
3 | 2 | rexlimdv 2409 | 1 ⊢ (φ → (∃x ∈ A ψ → χ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1375 ∃wrex 2284 |
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 1316 ax-gen 1318 ax-ie1 1364 ax-ie2 1365 ax-4 1382 ax-17 1401 ax-ial 1410 ax-i5r 1411 |
This theorem depends on definitions: df-bi 110 df-nf 1330 df-ral 2288 df-rex 2289 |
This theorem is referenced by: rexlimdvaa 2411 rexlimivv 2415 rexlimdvv 2416 ralxfrd 4142 rexxfrd 4143 fvelimab 5152 foco2 5241 elunirn 5328 f1elima 5335 tfrlem5 5847 tfrlemibacc 5856 tfrlemibfn 5858 nnaordex 6006 nnawordex 6007 ectocld 6076 ltexnqq 6253 ltbtwnnqq 6259 prarloclem4 6335 genprndl 6353 |
Copyright terms: Public domain | W3C validator |