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 2536 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2128 ∀wral 2435 |
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 1427 ax-gen 1429 ax-4 1490 ax-17 1506 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-ral 2440 |
This theorem is referenced by: ralxfrd 4422 isoselem 5770 isosolem 5774 findcard 6833 nnsub 8872 supinfneg 9506 infsupneg 9507 ublbneg 9522 expnlbnd2 10543 cau3lem 11014 climshftlemg 11199 subcn2 11208 serf0 11249 sqrt2irr 12037 tgcn 12619 tgcnp 12620 lmconst 12627 cnntr 12636 lmss 12657 txdis 12688 txlm 12690 blbas 12844 metss 12905 metcnp3 12922 iswomni0 13633 |
Copyright terms: Public domain | W3C validator |