|   | 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 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-ral 3062 | 
| This theorem is referenced by: r19.30OLD 3121 ralimdaa 3260 mpteqb 7035 tz7.49 8485 mptelixpg 8975 resixpfo 8976 bnd 9932 kmlem12 10202 lbzbi 12978 r19.29uz 15389 caubnd 15397 alzdvds 16357 ptclsg 23623 isucn2 24288 fusgreghash2wsp 30357 omssubadd 34302 subgrwlk 35137 dfon2lem8 35791 fvineqsneq 37413 dford3lem2 43039 neik0pk1imk0 44060 grur1cld 44251 mnuprdlem4 44294 mnurndlem1 44300 | 
| Copyright terms: Public domain | W3C validator |