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 2549 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2141 ∀wral 2448 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-ral 2453 |
This theorem is referenced by: ralxfrd 4447 isoselem 5799 isosolem 5803 findcard 6866 nnsub 8917 supinfneg 9554 infsupneg 9555 ublbneg 9572 expnlbnd2 10601 cau3lem 11078 climshftlemg 11265 subcn2 11274 serf0 11315 sqrt2irr 12116 pclemub 12241 prmpwdvds 12307 grpinveu 12741 tgcn 13002 tgcnp 13003 lmconst 13010 cnntr 13019 lmss 13040 txdis 13071 txlm 13073 blbas 13227 metss 13288 metcnp3 13305 iswomni0 14083 |
Copyright terms: Public domain | W3C validator |