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 2419 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ∃wrex 2307 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 df-rex 2312 |
This theorem is referenced by: r19.12 2422 reusv3 4192 rexxfrd 4195 iunpw 4211 fvelima 5225 carden2bex 6369 prnmaddl 6588 prarloclem5 6598 prarloc2 6602 genprndl 6619 genprndu 6620 ltpopr 6693 recexprlemm 6722 recexprlemopl 6723 recexprlemopu 6725 recexprlem1ssl 6731 recexprlem1ssu 6732 cauappcvgprlemupu 6747 caucvgprlemupu 6770 caucvgprprlemupu 6798 caucvgsrlemoffres 6884 resqrexlemgt0 9618 subcn2 9832 |
Copyright terms: Public domain | W3C validator |