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 416 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | ralimia 3085 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2112 ∀wral 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ral 3069 |
This theorem is referenced by: ralrnmptw 6935 ralrnmpt 6937 tz7.48-2 8202 mptelixpg 8640 boxriin 8645 acnlem 9692 iundom2g 10184 konigthlem 10212 hashge2el2dif 14079 rlim2 15090 prdsbas3 17019 prdsdsval2 17022 ptbasfi 22510 ptunimpt 22524 voliun 24483 lgamgulmlem6 25948 riesz4i 30176 dmdbr6ati 30536 ctbssinf 35351 |
Copyright terms: Public domain | W3C validator |