|   | 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 1810 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | 
| 3 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 4 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
| 5 | 2, 3, 4 | 3imtr4i 292 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ral 3061 | 
| This theorem is referenced by: ralimia 3079 ralcom3OLD 3097 tfi 7875 resixpfo 8977 omex 9684 kmlem1 10192 brdom5 10570 brdom4 10571 xrub 13355 pcmptcl 16930 itgeq2 25814 iblcnlem 25825 pntrsumbnd 27611 nmounbseqi 30797 nmounbseqiALT 30798 sumdmdi 32440 dmdbr4ati 32441 dmdbr6ati 32443 bnj110 34873 fiinfi 43591 | 
| Copyright terms: Public domain | W3C validator |