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 3159. (Revised by Wolf Lammen, 1-Dec-2019.) |
Ref | Expression |
---|---|
ral2imi.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ral2imi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | ral2imi.1 | . . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 2 | imim3i 64 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | al2imi 1807 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))) |
5 | df-ral 3140 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
6 | df-ral 3140 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)) | |
7 | 4, 5, 6 | 3imtr4g 297 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
8 | 1, 7 | sylbi 218 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: ralim 3159 ralbi 3164 r19.26 3167 rexim 3238 iiner 8358 ss2ixp 8462 undifixp 8486 boxriin 8492 acni2 9460 axcc4 9849 intgru 10224 ingru 10225 prdsdsval3 16746 mndind 17980 hauscmplem 21942 uspgr2wlkeq 27354 wlkp1lem8 27389 prdstotbnd 34953 mnuunid 40490 |
Copyright terms: Public domain | W3C validator |