|   | 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 3080 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∀wral 3061 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 | 
| This theorem is referenced by: ralrnmptw 7114 ralrnmpt 7116 tz7.48-2 8482 mptelixpg 8975 boxriin 8980 acnlem 10088 iundom2g 10580 konigthlem 10608 hashge2el2dif 14519 rlim2 15532 prdsbas3 17526 prdsdsval2 17529 ptbasfi 23589 ptunimpt 23603 voliun 25589 lgamgulmlem6 27077 riesz4i 32082 dmdbr6ati 32442 ctbssinf 37407 | 
| Copyright terms: Public domain | W3C validator |