![]() |
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 3085 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-ral 3062 |
This theorem is referenced by: r19.30OLD 3121 ralimdaa 3257 mpteqb 7014 tz7.49 8441 mptelixpg 8925 resixpfo 8926 bnd 9883 kmlem12 10152 lbzbi 12916 r19.29uz 15293 caubnd 15301 alzdvds 16259 ptclsg 23110 isucn2 23775 fusgreghash2wsp 29580 omssubadd 33287 subgrwlk 34111 dfon2lem8 34750 fvineqsneq 36281 dford3lem2 41751 neik0pk1imk0 42783 grur1cld 42976 mnuprdlem4 43019 mnurndlem1 43025 |
Copyright terms: Public domain | W3C validator |