![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimdva | 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 2426 | 1 ⊢ (φ → (∃x ∈ A ψ → χ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1390 ∃wrex 2301 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-i5r 1425 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-ral 2305 df-rex 2306 |
This theorem is referenced by: rexlimdvaa 2428 rexlimivv 2432 rexlimdvv 2433 ralxfrd 4160 rexxfrd 4161 fvelimab 5172 foco2 5261 elunirn 5348 f1elima 5355 tfrlem5 5871 tfrlemibacc 5881 tfrlemibfn 5883 nnaordex 6036 nnawordex 6037 ectocld 6108 ltexnqq 6391 ltbtwnnqq 6398 prarloclem4 6481 prarloc2 6487 genprndl 6504 genprndu 6505 prmuloc2 6548 1idprl 6566 1idpru 6567 cauappcvgprlemdisj 6623 cauappcvgprlemladdru 6628 cauappcvgprlemladdrl 6629 caucvgprlemladdrl 6649 recexgt0sr 6701 cnegexlem1 6983 cnegexlem2 6984 renegcl 7068 qmulz 8334 icc0r 8565 frec2uzrand 8872 frecuzrdgfn 8879 |
Copyright terms: Public domain | W3C validator |