![]() |
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 2514 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1481 ∀wral 2417 |
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 1424 ax-gen 1426 ax-4 1488 ax-17 1507 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-ral 2422 |
This theorem is referenced by: ralxfrd 4391 isoselem 5729 isosolem 5733 findcard 6790 nnsub 8783 supinfneg 9417 infsupneg 9418 ublbneg 9432 expnlbnd2 10448 cau3lem 10918 climshftlemg 11103 subcn2 11112 serf0 11153 sqrt2irr 11876 tgcn 12416 tgcnp 12417 lmconst 12424 cnntr 12433 lmss 12454 txdis 12485 txlm 12487 blbas 12641 metss 12702 metcnp3 12719 |
Copyright terms: Public domain | W3C validator |