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 2948. (Revised by Wolf Lammen, 1-Dec-2019.) |
Ref | Expression |
---|---|
ral2imi.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ral2imi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2917 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | ral2imi.1 | . . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 2 | imim3i 64 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | al2imi 1743 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))) |
5 | df-ral 2917 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
6 | df-ral 2917 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)) | |
7 | 4, 5, 6 | 3imtr4g 285 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
8 | 1, 7 | sylbi 207 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: ralim 2948 rexim 3008 r19.26 3064 iiner 7819 ss2ixp 7921 undifixp 7944 boxriin 7950 acni2 8869 axcc4 9261 intgru 9636 ingru 9637 prdsdsval3 16145 mrcmndind 17366 hauscmplem 21209 uspgr2wlkeq 26542 wlkp1lem8 26577 prdstotbnd 33593 |
Copyright terms: Public domain | W3C validator |