![]() |
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 414 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | ralimia 3080 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ral 3062 |
This theorem is referenced by: ralrnmptw 7045 ralrnmpt 7047 tz7.48-2 8389 mptelixpg 8876 boxriin 8881 acnlem 9989 iundom2g 10481 konigthlem 10509 hashge2el2dif 14385 rlim2 15384 prdsbas3 17368 prdsdsval2 17371 ptbasfi 22948 ptunimpt 22962 voliun 24934 lgamgulmlem6 26399 riesz4i 31047 dmdbr6ati 31407 ctbssinf 35923 |
Copyright terms: Public domain | W3C validator |