![]() |
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 1808 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3060 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 292 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ∈ wcel 2106 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-ral 3060 |
This theorem is referenced by: ralimia 3078 ralcom3OLD 3096 tfi 7874 resixpfo 8975 omex 9681 kmlem1 10189 brdom5 10567 brdom4 10568 xrub 13351 pcmptcl 16925 itgeq2 25828 iblcnlem 25839 pntrsumbnd 27625 nmounbseqi 30806 nmounbseqiALT 30807 sumdmdi 32449 dmdbr4ati 32450 dmdbr6ati 32452 bnj110 34851 fiinfi 43563 |
Copyright terms: Public domain | W3C validator |