Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimdva | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) |
Ref | Expression |
---|---|
ralrimdva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralrimdva | ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimdva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
2 | 1 | ex 114 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 2488 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1465 ∀wral 2393 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 |
This theorem is referenced by: ralxfrd 4353 isoselem 5689 isosolem 5693 findcard 6750 nnsub 8727 supinfneg 9358 infsupneg 9359 ublbneg 9373 expnlbnd2 10385 cau3lem 10854 climshftlemg 11039 subcn2 11048 serf0 11089 sqrt2irr 11767 tgcn 12304 tgcnp 12305 lmconst 12312 cnntr 12321 lmss 12342 txdis 12373 txlm 12375 blbas 12529 metss 12590 metcnp3 12607 |
Copyright terms: Public domain | W3C validator |