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 3153 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: ralimdaa 3214 r19.30 3335 r19.30OLD 3336 mpteqb 6779 tz7.49 8070 mptelixpg 8487 resixpfo 8488 bnd 9309 kmlem12 9575 lbzbi 12324 r19.29uz 14698 caubnd 14706 alzdvds 15658 ptclsg 22151 isucn2 22815 fusgreghash2wsp 28044 omssubadd 31457 subgrwlk 32276 dfon2lem8 32932 fvineqsneq 34575 dford3lem2 39502 neik0pk1imk0 40275 grur1cld 40445 mnuprdlem4 40488 mnurndlem1 40494 |
Copyright terms: Public domain | W3C validator |