![]() |
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 3087. (Revised by Wolf Lammen, 1-Dec-2019.) |
Ref | Expression |
---|---|
ral2imi.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ral2imi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 3063 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | ral2imi.1 | . . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 2 | imim3i 64 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | al2imi 1817 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))) |
5 | df-ral 3063 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
6 | df-ral 3063 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)) | |
7 | 4, 5, 6 | 3imtr4g 295 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
8 | 1, 7 | sylbi 216 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ∈ wcel 2106 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-ral 3063 |
This theorem is referenced by: ralim 3087 rexim 3088 ralbi 3104 r19.26 3112 iiner 8686 ss2ixp 8806 undifixp 8830 boxriin 8836 acni2 9940 axcc4 10333 intgru 10708 ingru 10709 prdsdsval3 17327 mndind 18598 hauscmplem 22709 uspgr2wlkeq 28423 wlkp1lem8 28457 prdstotbnd 36191 mnuunid 42468 |
Copyright terms: Public domain | W3C validator |