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 2947 | 1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: ralimdaa 2958 r19.30 3082 trint 4768 mpteqb 6299 tz7.49 7540 mptelixpg 7945 resixpfo 7946 bnd 8755 kmlem12 8983 lbzbi 11776 r19.29uz 14090 caubnd 14098 alzdvds 15042 ptclsg 21418 isucn2 22083 fusgreghash2wsp 27202 omssubadd 30362 dfon2lem8 31695 dford3lem2 37594 neik0pk1imk0 38345 |
Copyright terms: Public domain | W3C validator |