![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reximdv | GIF version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.) |
Ref | Expression |
---|---|
reximdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
reximdv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | a1d 22 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
3 | 2 | reximdvai 2491 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ∃wrex 2376 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-ral 2380 df-rex 2381 |
This theorem is referenced by: r19.12 2497 reusv3 4319 rexxfrd 4322 iunpw 4339 fvelima 5405 carden2bex 6956 prnmaddl 7199 prarloclem5 7209 prarloc2 7213 genprndl 7230 genprndu 7231 ltpopr 7304 recexprlemm 7333 recexprlemopl 7334 recexprlemopu 7336 recexprlem1ssl 7342 recexprlem1ssu 7343 cauappcvgprlemupu 7358 caucvgprlemupu 7381 caucvgprprlemupu 7409 caucvgsrlemoffres 7495 resqrexlemgt0 10632 subcn2 10919 bezoutlembz 11485 tgcl 12015 neiss 12101 ssnei2 12108 tgcnp 12159 cnptopco 12172 cnptopresti 12188 lmtopcnp 12200 blssexps 12357 blssex 12358 mopni3 12412 neibl 12419 metss 12422 metcnp3 12435 rescncf 12481 limcresi 12515 |
Copyright terms: Public domain | W3C validator |