|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ralimdaa | Structured version Visualization version GIF version | ||
| Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.) | 
| Ref | Expression | 
|---|---|
| ralimdaa.1 | ⊢ Ⅎ𝑥𝜑 | 
| ralimdaa.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| ralimdaa | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ralimdaa.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
| 2 | ralimdaa.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
| 3 | 2 | ex 412 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | 
| 4 | 1, 3 | ralrimi 3256 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) | 
| 5 | ralim 3085 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | |
| 6 | 4, 5 | syl 17 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1782 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 df-ral 3061 | 
| This theorem is referenced by: ralbida 3269 eltsk2g 10792 ptcnplem 23630 poimirlem26 37654 allbutfifvre 45695 climleltrp 45696 fnlimabslt 45699 limsupub2 45832 liminflbuz2 45835 xlimmnfvlem1 45852 xlimmnfvlem2 45853 xlimpnfvlem1 45856 xlimpnfvlem2 45857 stoweidlem61 46081 stoweid 46083 fourierdlem73 46199 smflimlem2 46792 | 
| Copyright terms: Public domain | W3C validator |