![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralim | Structured version Visualization version GIF version |
Description: Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
Ref | Expression |
---|---|
ralim | ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | ral2imi 3083 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-ral 3060 |
This theorem is referenced by: r19.30OLD 3119 ralimdaa 3258 mpteqb 7035 tz7.49 8484 mptelixpg 8974 resixpfo 8975 bnd 9930 kmlem12 10200 lbzbi 12976 r19.29uz 15386 caubnd 15394 alzdvds 16354 ptclsg 23639 isucn2 24304 fusgreghash2wsp 30367 omssubadd 34282 subgrwlk 35117 dfon2lem8 35772 fvineqsneq 37395 dford3lem2 43016 neik0pk1imk0 44037 grur1cld 44228 mnuprdlem4 44271 mnurndlem1 44277 |
Copyright terms: Public domain | W3C validator |