| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ral2imi | Structured version Visualization version GIF version | ||
| Description: Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3086. (Revised by Wolf Lammen, 1-Dec-2019.) |
| Ref | Expression |
|---|---|
| ral2imi.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| ral2imi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 2 | ral2imi.1 | . . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 3 | 2 | imim3i 64 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))) |
| 4 | 3 | al2imi 1815 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))) |
| 5 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
| 6 | df-ral 3062 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)) | |
| 7 | 4, 5, 6 | 3imtr4g 296 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| 8 | 1, 7 | sylbi 217 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∈ 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-ral 3062 |
| This theorem is referenced by: ralim 3086 rexim 3087 ralbi 3103 r19.26 3111 iiner 8829 ss2ixp 8950 undifixp 8974 boxriin 8980 acni2 10086 axcc4 10479 intgru 10854 ingru 10855 prdsdsval3 17530 mndind 18841 hauscmplem 23414 uspgr2wlkeq 29664 wlkp1lem8 29698 prdstotbnd 37801 mnuunid 44296 |
| Copyright terms: Public domain | W3C validator |