![]() |
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 115 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 2556 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 |
This theorem is referenced by: ralxfrd 4464 isoselem 5824 isosolem 5828 findcard 6891 nnsub 8961 supinfneg 9598 infsupneg 9599 ublbneg 9616 expnlbnd2 10649 cau3lem 11126 climshftlemg 11313 subcn2 11322 serf0 11363 sqrt2irr 12165 pclemub 12290 prmpwdvds 12356 grpinveu 12917 dfgrp3mlem 12974 issubg4m 13059 tgcn 13848 tgcnp 13849 lmconst 13856 cnntr 13865 lmss 13886 txdis 13917 txlm 13919 blbas 14073 metss 14134 metcnp3 14151 iswomni0 14940 |
Copyright terms: Public domain | W3C validator |