![]() |
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 8446 mptelixpg 8933 boxriin 8938 acnlem 10047 iundom2g 10539 konigthlem 10567 hashge2el2dif 14446 rlim2 15445 prdsbas3 17432 prdsdsval2 17435 ptbasfi 23306 ptunimpt 23320 voliun 25304 lgamgulmlem6 26775 riesz4i 31584 dmdbr6ati 31944 ctbssinf 36591 |
Copyright terms: Public domain | W3C validator |