![]() |
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 412 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | ralimia 3079 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3061 |
This theorem is referenced by: ralrnmptw 7095 ralrnmpt 7097 tz7.48-2 8448 mptelixpg 8935 boxriin 8940 acnlem 10049 iundom2g 10541 konigthlem 10569 hashge2el2dif 14448 rlim2 15447 prdsbas3 17434 prdsdsval2 17437 ptbasfi 23404 ptunimpt 23418 voliun 25402 lgamgulmlem6 26878 riesz4i 31748 dmdbr6ati 32108 ctbssinf 36750 |
Copyright terms: Public domain | W3C validator |