![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimi2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
Ref | Expression |
---|---|
ralimi2.1 | ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
ralimi2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) | |
2 | 1 | alimi 1805 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3051 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3051 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 291 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ral 3051 |
This theorem is referenced by: ralimia 3069 ralcom3OLD 3087 tfi 7862 resixpfo 8964 omex 9682 kmlem1 10189 brdom5 10568 brdom4 10569 xrub 13340 pcmptcl 16888 itgeq2 25790 iblcnlem 25801 pntrsumbnd 27587 nmounbseqi 30702 nmounbseqiALT 30703 sumdmdi 32345 dmdbr4ati 32346 dmdbr6ati 32348 bnj110 34671 fiinfi 43189 |
Copyright terms: Public domain | W3C validator |