![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimiaa | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
Ref | Expression |
---|---|
ralimiaa.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) |
Ref | Expression |
---|---|
ralimiaa | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimiaa.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) | |
2 | 1 | ex 403 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | ralimia 3131 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2106 ∀wral 3089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ral 3094 |
This theorem is referenced by: ralrnmpt 6632 tz7.48-2 7820 mptelixpg 8231 boxriin 8236 acnlem 9204 iundom2g 9697 konigthlem 9725 hashge2el2dif 13576 rlim2 14635 prdsbas3 16527 prdsdsval2 16530 ptbasfi 21793 ptunimpt 21807 voliun 23758 lgamgulmlem6 25212 riesz4i 29494 dmdbr6ati 29854 |
Copyright terms: Public domain | W3C validator |